This commit is contained in:
Simon Cruanes 2016-07-28 10:47:59 +02:00
parent ac706f3e56
commit eb14a1e229

View file

@ -663,7 +663,7 @@ module Make
(* visit the current predecessors *)
for j = 0 to Array.length !c.atoms - 1 do
let q = !c.atoms.(j) in
assert (q.is_true || q.neg.is_true && q.var.v_level >= env.base_level); (* unsure? *)
assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *)
if q.var.v_level <= env.base_level then begin
assert (q.neg.is_true);
match q.var.reason with