Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 82621efd authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'next' into new_ide

# Conflicts:
#	examples/tests-provers/bv/why3session.xml
#	examples/tests-provers/div/why3session.xml
#	examples/tests-provers/ieee_float/why3session.xml
#	src/printer/smtv2.ml
parents fe8c2bf3 83d52488
......@@ -44,6 +44,11 @@ transformation "encoding_smt_if_poly"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
(** Z3 needs "(push)" to provide models *)
theory BuiltIn
meta "counterexample_need_smtlib_push" ""
end
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
......
......@@ -129,6 +129,7 @@ type info = {
mutable list_projs : Stdlib.Sstr.t;
meta_model_projection : Sls.t;
mutable list_records : ((string * string) list) Stdlib.Mstr.t;
info_cntexample_need_push : bool;
}
let debug_print_term message t =
......@@ -512,7 +513,7 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
info.info_in_goal <- true;
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
info.info_in_goal <- false;
(*if cntexample then fprintf fmt "@[(push)@]@\n"; (* z3 specific stuff *)*)
if cntexample && info.info_cntexample_need_push then fprintf fmt "@[(push)@]@\n";
fprintf fmt "@[(check-sat)@]@\n";
let model_list = print_info_model cntexample fmt info in
......@@ -592,8 +593,16 @@ let set_produce_models fmt cntexample =
if cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let meta_counterexmp_need_push =
Theory.register_meta_excl "counterexample_need_smtlib_push" [Theory.MTstring]
~desc:"Internal@ use@ only"
let print_task args ?old:_ fmt task =
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let need_push =
let need_push_meta = Task.find_meta_tds task meta_counterexmp_need_push in
not (Theory.Stdecl.is_empty need_push_meta.Task.tds_set)
in
let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
let vc_info = {vc_inside = false; vc_loc = None; vc_func_name = None} in
let info = {
......@@ -607,7 +616,9 @@ let print_task args ?old:_ fmt task =
list_projs = Stdlib.Sstr.empty;
meta_model_projection = Task.on_tagged_ls meta_projection task;
list_records = Stdlib.Mstr.empty;
} in
info_cntexample_need_push = need_push;
}
in
print_prelude fmt args.prelude;
set_produce_models fmt cntexample;
print_th_prelude task fmt args.th_prelude;
......
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