diff --git a/src/verification.ml b/src/verification.ml
index 3319b637c4fe42c37fa86e182524a79ac2acee3b..1aeefd3a141e2a807db5da966615eb858117ba92 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 b65e81398bbda39ead2a04f662643b1daac67d34..a67656301fd0d8f73aeb3801aef55a18b02de652 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: