diff --git a/src/verification.ml b/src/verification.ml index 3139df410cb82ebb58e6f4fccaccee73eaec09e9..ae1df7cb3d5ea5fc359e403610b84bd5ffc73d15 100644 --- a/src/verification.ml +++ b/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 = diff --git a/tests/marabou.t b/tests/marabou.t index d0e071ce568abe5d1cffba5f1b5ad25d1aee89bf..7379622e4bc5f10d156e130443f0b868bf4f66cc 100644 --- a/tests/marabou.t +++ b/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 () diff --git a/tests/simple.t b/tests/simple.t index 8bc9aa3f18f4e52272066cb5ef738f36baee17d9..e908b61d8fa8eda7d2c269e9f335586750c070ad 100644 --- a/tests/simple.t +++ b/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 () diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t index 90e92776592749fd819ced349420f7f209202b8a..30d2d720a3c7850e6ef9267d9e733472f66f1683 100644 --- a/tests/simple_onnx.t +++ b/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 () diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t index 2561471424f309a88e24e8b976d50f9f1989951e..34a460815ce62de6965ca880ee0d908c055336a1 100644 --- a/tests/simple_ovo.t +++ b/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