From 80ca21910c676a9efd0fdd68f2324e56029e709e Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 5 Sep 2022 16:04:09 +0200
Subject: [PATCH] Use Logs.app function for displaying verification results.
---
src/verification.ml | 5 +++--
tests/marabou.t | 6 ++----
tests/simple.t | 6 ++----
tests/simple_onnx.t | 3 +--
tests/simple_ovo.t | 2 +-
5 files changed, 9 insertions(+), 13 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 3139df4..ae1df7c 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 d0e071c..7379622 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 8bc9aa3..e908b61 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 90e9277..30d2d72 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 2561471..34a4608 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
--
GitLab