Test

src/lib/reasoners/satml.ml

@@ -47,6 +47,10 @@ type conflict_origin =
 
 let vraie_form = E.vrai
 
+let pp str =
+  if Options.get_verbose () then
+    Format.printf str
+  else Format.ifprintf Format.std_formatter str
 
 module type SAT_ML = sig
   (*module Make (Dummy : sig end) : sig*)
@@ -597,6 +601,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     !max_lvl
 
   let enqueue env (a : Atom.atom) lvl reason =
+    pp "Enqueue!@.";
     assert (not a.is_true && not a.neg.is_true &&
             a.var.level < 0 && a.var.reason == None && lvl >= 0);
     if a.neg.is_guard then begin
@@ -1826,15 +1831,18 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0
 
   let pop env =
+    pp "pop: is increm guards empty?@.";
     (assert (not (Vec.is_empty env.increm_guards)));
     let g = Vec.pop env.increm_guards in
     env.is_unsat <- env.is_unsat_cpt <> 0;
     env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1);
     g.is_guard <- false;
     g.neg.is_guard <- false;
+    pp "pop: is atom %a true?@." Atom.pr_atom g.var.na;
     assert (not g.var.na.is_true); (* atom not false *)
     if g.var.pa.is_true then (* if already decided  *)
       begin
+        pp "pop: var level = %i@." g.var.level;
         (assert (g.var.level > 0));
         cancel_until env (g.var.level - 1); (* undo its decision *)
         (* all previous guards are decided *)

tests/cram.t/run.t

@@ -27,7 +27,7 @@ Now we will test some semantic triggers.
 
 And some SMT2 action.
 
-  $ alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null
+  $ OCAMLRUNPARAM=b alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 --debug sat --verbose
 
   unknown