Commit 2bd9354f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

hopefully final commmit before release 0.73

parent a8a44982
* marks an incompatible change * marks an incompatible change
o [Provers] support for Z3 4.0
o [Sessions] a small change in the format. Why3 is still able to o [Sessions] a small change in the format. Why3 is still able to
read session files in the old format. read session files in the old format.
o completed support for the "Out Of Memory" prover result o completed support for the "Out Of Memory" prover result
......
...@@ -625,15 +625,15 @@ if test "$enable_coq_support" = "yes" ; then ...@@ -625,15 +625,15 @@ if test "$enable_coq_support" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs" echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
fi fi
fi fi
echo "PVS support : $enable_pvs_support $reason_pvs_support" dnl echo "PVS support : $enable_pvs_support $reason_pvs_support"
if test "$enable_pvs_support" = "yes" ; then dnl if test "$enable_pvs_support" = "yes" ; then
echo " Version : $PVSVERSION" dnl echo " Version : $PVSVERSION"
echo " Lib : $PVSLIB" dnl echo " Lib : $PVSLIB"
echo " Realization support : $enable_pvs_libs $reason_pvs_libs" dnl echo " Realization support : $enable_pvs_libs $reason_pvs_libs"
if test "$enable_pvs_libs" = "yes" ; then dnl if test "$enable_pvs_libs" = "yes" ; then
echo " FP arithmetic : $enable_pvs_fp_libs $reason_pvs_fp_libs" dnl echo " FP arithmetic : $enable_pvs_fp_libs $reason_pvs_fp_libs"
fi dnl fi
fi dnl fi
echo "hypothesis selection : $enable_hypothesis_selection" echo "hypothesis selection : $enable_hypothesis_selection"
echo "debugging symbols : $enable_debug" echo "debugging symbols : $enable_debug"
echo "profiling : $enable_profiling" echo "profiling : $enable_profiling"
......
...@@ -225,21 +225,7 @@ end ...@@ -225,21 +225,7 @@ end
module M = Session_scheduler.Make(O) module M = Session_scheduler.Make(O)
let print_result fmt let print_result = Call_provers.print_prover_result
{ Call_provers.pr_answer=ans;
Call_provers.pr_output=out;
Call_provers.pr_time=t } =
fprintf fmt "%a (%.1fs)" Call_provers.print_prover_answer ans t;
(*
fprintf fmt "%a" Call_provers.print_prover_answer ans;
*)
match ans with
| Call_provers.HighFailure ->
fprintf fmt "@\nProver output:@\n%s@." out
| _ -> ()
(*
fprintf fmt "[limit=%s@\nProver output:@\n%s@." out
*)
let main_loop = O.main_loop let main_loop = O.main_loop
......
Supports Markdown
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