Commit 1628b802 authored by David Hauzar's avatar David Hauzar

Ask for reason why a smt prover response unknown only for counterexamples.

parent e28f4cda
......@@ -582,8 +582,10 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
let model_list = S.elements info.info_model in
fprintf fmt "@[(check-sat)@]@\n";
print_info_model cntexample fmt model_list info;
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
if cntexample then begin
(* (get-info :reason-unknown) *)
fprintf fmt "@[(get-info :reason-unknown)@]@\n";
end;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
......
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