simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 19:25:36 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix bug

Browse source
This commit is contained in:
Simon Cruanes 2016-07-29 20:45:30 +02:00
parent 85c290c0ce
commit 6eeaa8513c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/internal.ml
View file

@ -636,7 +636,7 @@ module Make
for j = 0 to Array.length !c.atoms - 1 do for j = 0 to Array.length !c.atoms - 1 do
let q = !c.atoms.(j) in let q = !c.atoms.(j) in
assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* 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 if q.var.v_level <= 0 then begin
assert (q.neg.is_true); assert (q.neg.is_true);
match q.var.reason with match q.var.reason with
| Some Bcp cl -> history := cl :: !history | Some Bcp cl -> history := cl :: !history
@ -645,7 +645,7 @@ module Make
if not q.var.seen then begin if not q.var.seen then begin
q.var.seen <- true; q.var.seen <- true;
seen := q :: !seen; 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; var_bump_activity q.var;
if q.var.v_level >= decision_level () then begin if q.var.v_level >= decision_level () then begin
incr pathC incr pathC