From 4d8ab09be06d6c27be73dac84125c420f97c7c74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 7 Dec 2021 16:11:03 +0100
Subject: [PATCH] Remove prover output from caisar output
---
src/verification.ml | 3 +--
tests/marabout.t | 9 ---------
tests/simple.t | 21 ---------------------
3 files changed, 1 insertion(+), 32 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index cb38ab34..aaf623e0 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 db5c02bc..78194e3b 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 7b41c27d..14221315 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
-
--
GitLab