Use Logs.app function for displaying verification results.

src/verification.ml

@@ -198,8 +198,9 @@ let call_prover ~limit config (prover : Whyconf.config_prover) driver env
     then answer_saver limit config task env prover dataset_csv
     else answer_generic limit config task driver prover
   in
-  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
-    Call_provers.print_prover_answer prover_answer
+  Logs.app (fun m ->
+    m "@[Goal %a:@ %a@]" Pretty.print_pr (Task.task_goal task)
+      Call_provers.print_prover_answer prover_answer)
 
 let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
   ?dataset_csv file =

tests/marabou.t

@@ -34,7 +34,5 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
-  Goal H: Unknown
-  ()
+  [caisar] Goal G: Unknown ()
+  [caisar] Goal H: Unknown ()

tests/simple.t

@@ -37,7 +37,5 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
-  Goal H: Unknown
-  ()
+  [caisar] Goal G: Unknown ()
+  [caisar] Goal H: Unknown ()

tests/simple_onnx.t

@@ -29,5 +29,4 @@ Test verify
   >      (0.0:t) .< y1 .< (0.5:t)
   > end
   > EOF
-  Goal G: Unknown
-  ()
+  [caisar] Goal G: Unknown ()

tests/simple_ovo.t

@@ -34,4 +34,4 @@ Test verify
   >   goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
   > end
   > EOF
-  Goal G: High failure
+  [caisar] Goal G: High failure