Commit 3e11712e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make why3prove error out on unproven goals.

This commit also increases the bench timeout to 15 seconds to avoid
spurious failures on CI slaves, since McCarthy91Mach.f91_nonrec takes
about 5 seconds on a fast computer.
parent ccf01756
......@@ -77,14 +77,13 @@ valid_goals () {
for f in $1/*.mlw; do
printf " $f... "
if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
echo "valid test $f failed!"
echo "$pgm -P alt-ergo $f"
$pgm -t 10 -P alt-ergo $f
if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
echo "FAILED!"
echo "$pgm -t 15 -P alt-ergo $f"
$pgm -t 15 -P alt-ergo $f
exit 1
echo "ok"
echo "ok"
......@@ -244,6 +244,8 @@ let output_task drv fname _tname th task dir =
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let unproved = ref false
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let limit =
{ Call_provers.empty_limit with
......@@ -256,7 +258,8 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let res = Call_provers.wait_on_call call in
printf "%s %s %s: %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
Call_provers.print_prover_result res;
if res.Call_provers.pr_answer <> Call_provers.Valid then unproved := true
| None, None ->
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
......@@ -357,7 +360,8 @@ let () =
let load (f,ef) = load_driver (Whyconf.get_main config) env f ef in
let drv = load !opt_driver in
Queue.iter (do_input env drv) opt_queue
Queue.iter (do_input env drv) opt_queue;
if !unproved then exit 1
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment