From 4cc257995eb8a92a8058866b7ea1efe54a5e42af Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 22 Nov 2021 15:00:57 +0100
Subject: [PATCH] Do not print the amount of time for proving.

---
 src/verification.ml | 4 ++--
 tests/simple.t      | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/verification.ml b/src/verification.ml
index 3319b637..1aeefd3a 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -44,8 +44,8 @@ let call_prover ~limit prover driver task =
   in
   let prover_result = Call_provers.wait_on_call prover_call in
   Fmt.pr "Goal %a: %a@.Output:@.%s@." Pretty.print_pr (Task.task_goal task)
-    (Call_provers.print_prover_result ~json:false)
-    prover_result prover_result.pr_output
+    Call_provers.print_prover_answer prover_result.pr_answer
+    prover_result.pr_output
 
 let verify format loadpath ?memlimit ~prover file =
   let open Why3 in
diff --git a/tests/simple.t b/tests/simple.t
index b65e8139..a6765630 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -48,8 +48,8 @@ Test verify
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
   <autodetect>3 prover(s) added
-  Goal G: Unknown ()
-  (0.00s)
+  Goal G: Unknown
+  ()
   Output:
   NN: ./TestNetwork.nnet
   Goal:
@@ -59,8 +59,8 @@ Test verify
   y0 <  0.5
   Result = Unknown
   
-  Goal H: Unknown ()
-  (0.00s)
+  Goal H: Unknown
+  ()
   Output:
   NN: ./TestNetwork.nnet
   Goal:
-- 
GitLab