From 72968f9d3ac32bbca001a4675436bad912d8e391 Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Thu, 14 Dec 2023 10:37:11 +0100
Subject: [PATCH] Test

---
 src/lib/reasoners/satml.ml | 24 +++++++++++++++++++++---
 tests/cram.t/run.t         |  2 +-
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 7d2c79976c..f83bccb766 100644
--- a/src/lib/reasoners/satml.ml
+++ b/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,36 @@ 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
+    else begin
+      pp "Is next dec guard (%i) = 0?@." env.next_dec_guard;
+      (assert (env.next_dec_guard = 0))
+    end;
+    pp "Calling enqueue@.";
+    enqueue env g.neg 0 None;
+    pp "Good, let's leave pop now.@."
 
   let optimize env ~is_max obj = env.tenv <- Th.optimize env.tenv ~is_max obj
 end
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index bf837bf48a..c77aaab731 100644
--- a/tests/cram.t/run.t
+++ b/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