From 85c290c0ce93051f61d492cefb5179353c4a4acf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jul 2016 20:04:54 +0200 Subject: [PATCH] small changes --- src/core/internal.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index b5a42d9d..f2dfc015 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -296,7 +296,7 @@ module Make let a = atoms.(i) in if a.is_true then let l = a.var.v_level in - if 0 <= l && l <= root then + if l = 0 then raise Trivial (* A var true at level 0 gives a trivially true clause *) else (a :: trues) @ unassigned @ falses @ @@ -530,6 +530,7 @@ module Make b.var.v_level ) else ( assert (a.var.v_level = b.var.v_level); + assert (a.var.v_level >= env.base_level); max (a.var.v_level - 1) env.base_level ) @@ -756,7 +757,7 @@ module Make (fun a b -> compare b.var.v_level a.var.v_level) clause.atoms; attach_clause clause; - add_boolean_conflict init + add_boolean_conflict clause end else begin attach_clause clause; if b.neg.is_true && not a.is_true && not a.neg.is_true then begin