diff --git a/src/verification.ml b/src/verification.ml
index cb38ab341e37bdc76bd2aa2ddd288f4338918724..aaf623e0fe9c325aa70053741590bfc3dc7f7e32 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -43,9 +43,8 @@ let call_prover ~limit prover driver task =
     Driver.prove_task_prepared ~command ~limit driver task_prepared
   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)
+  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
     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/marabout.t b/tests/marabout.t
index db5c02bccd1ad88e859caaf31682762d3b9ae946..78194e3b714a2b6f0fe5afd6ee7b14da311adb4b 100644
--- a/tests/marabout.t
+++ b/tests/marabout.t
@@ -40,12 +40,3 @@ Test verify
   <autodetect>3 prover(s) added
   Goal G: Unknown
   ()
-  Output:
-  NN: ./TestNetwork.nnet
-  Goal:
-  x0 >  0.0
-  x0 <  0.5
-  y0 >  0.0
-  y0 <  0.5
-  Unknown
-  
diff --git a/tests/simple.t b/tests/simple.t
index 7b41c27d4cfea8e64d257eb3418f3db299257035..14221315cd8cb35dc83f17a0f7eef5d982ac19a0 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -45,26 +45,5 @@ Test verify
   <autodetect>3 prover(s) added
   Goal G: Unknown
   ()
-  Output:
-  NN: ./TestNetwork.nnet
-  Goal:
-  0.0 <  x0
-  x0 <  0.5
-  0.0 <  y0
-  y0 <  0.5
-  Result = Unknown
-  
   Goal H: Unknown
   ()
-  Output:
-  NN: ./TestNetwork.nnet
-  Goal:
-  0.0 <  x0
-  x0 <  0.5
-  0.5 <  x1
-  x1 <  1.0
-  0.0 <  y0 or 0.5 <  y0
-  0.0 <  y1
-  y1 <  0.5
-  Result = Unknown
-