Skip to content
Snippets Groups Projects
Commit 4d8ab09b authored by François Bobot's avatar François Bobot
Browse files

Remove prover output from caisar output

parent 087329e0
No related branches found
No related tags found
No related merge requests found
...@@ -43,9 +43,8 @@ let call_prover ~limit prover driver task = ...@@ -43,9 +43,8 @@ let call_prover ~limit prover driver task =
Driver.prove_task_prepared ~command ~limit driver task_prepared Driver.prove_task_prepared ~command ~limit driver task_prepared
in in
let prover_result = Call_provers.wait_on_call prover_call 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 Call_provers.print_prover_answer prover_result.pr_answer
prover_result.pr_output
let verify format loadpath ?memlimit ~prover file = let verify format loadpath ?memlimit ~prover file =
let open Why3 in let open Why3 in
......
...@@ -40,12 +40,3 @@ Test verify ...@@ -40,12 +40,3 @@ Test verify
<autodetect>3 prover(s) added <autodetect>3 prover(s) added
Goal G: Unknown Goal G: Unknown
() ()
Output:
NN: ./TestNetwork.nnet
Goal:
x0 > 0.0
x0 < 0.5
y0 > 0.0
y0 < 0.5
Unknown
...@@ -45,26 +45,5 @@ Test verify ...@@ -45,26 +45,5 @@ Test verify
<autodetect>3 prover(s) added <autodetect>3 prover(s) added
Goal G: Unknown 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 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment