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.

bench/bench

@@ -59,14 +59,13 @@ valid_goals () {
     pgm="bin/why3prove$suffix"
     for f in $1/*.mlw; do
 	echo -n "  "$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
-       else
-	    echo "ok"
        fi
+       echo "ok"
     done
 }
 

src/tools/why3prove.ml

@@ -240,6 +240,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
@@ -252,7 +254,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
@@ -351,7 +354,8 @@ let () =
   try
     let load (f,ef) = load_driver (Whyconf.get_main config) env f ef in
     let drv = Opt.map 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