Test

src/lib/reasoners/satml.ml

@@ -84,6 +84,10 @@ type conflict_origin =
 (* not even the final one *)
 let vraie_form = E.vrai
 
+let pp m =
+  if Options.get_verbose () then
+    Format.printf m
+  else Format.ifprintf Format.std_formatter m
 
 module type SAT_ML = sig
   (*module Make (Dummy : sig end) : sig*)
@@ -1973,22 +1977,33 @@ 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;
-    assert (not g.var.na.is_true); (* atom not false *)
+    pp "pop: is atom %a true? %b@." Atom.pr_atom g.var.na g.var.na.is_true;
+    if g.var.na.is_true then
+      begin
+        pp "Looks like so, smells bad!@.";
+        assert false
+      end;
+    (* assert (not g.var.na.is_true); (\* atom not false *\) *)
+    pp "Good, let's keep going@.";
     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 *)
         env.next_dec_guard <- Vec.size env.increm_guards
       end
     else (assert (env.next_dec_guard = 0));
-    enqueue env g.neg 0 None
+    pp "Calling enqueue@.";
+    enqueue env g.neg 0 None;
+    Format.printf "Good, let's leave pop now.@."
 
   let optimize env ~is_max obj = env.tenv <- Th.optimize env.tenv ~is_max obj
 end

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 --verbose
 
   unknown