From 6eeaa8513ce6cda99fb3118bdad91431f6ad1bd9 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jul 2016 20:45:30 +0200 Subject: [PATCH] fix bug --- src/core/internal.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index f2dfc015..4e77b073 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -636,7 +636,7 @@ module Make 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 >= 0); (* unsure? *) - if q.var.v_level <= env.base_level then begin + if q.var.v_level <= 0 then begin assert (q.neg.is_true); match q.var.reason with | Some Bcp cl -> history := cl :: !history @@ -645,7 +645,7 @@ module Make if not q.var.seen then begin q.var.seen <- true; seen := q :: !seen; - if q.var.v_level > env.base_level then begin + if q.var.v_level > 0 then begin var_bump_activity q.var; if q.var.v_level >= decision_level () then begin incr pathC