diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index c4438e76..794e5e39 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -290,9 +290,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) raise Unsat let enqueue_bool a lvl reason = + L.debug 99 "Entering enqueue_bool"; assert (not a.neg.is_true); if a.is_true then - L.debug 10 "Litteral %a alreayd in queue" pp_atom a + L.debug 10 "Litteral %a already in queue" pp_atom a else begin assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); a.is_true <- true; @@ -303,6 +304,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) end let enqueue_assign v value lvl = + L.debug 99 "Entering enqueue_assign"; v.tag.assigned <- Some value; v.level <- lvl; Vec.push env.trail (Either.mk_left v);