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

Fixed bad decision level updating during pop

Browse source
This commit is contained in:
Guillaume Bury 2015-11-18 17:37:36 +01:00
parent 763d23146f
commit 6567d32900
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
solver/internal.ml
View file

@ -999,14 +999,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
done; done;
Th.backtrack th_env; (* recover the right tenv *) Th.backtrack th_env; (* recover the right tenv *)
Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
if not (Vec.is_empty env.trail_lim) then begin Vec.clear env.trail_lim;
Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - 1); Vec.clear env.tenv_queue;
Vec.set env.trail_lim 0 env.qhead
end;
if not (Vec.is_empty env.tenv_queue) then begin
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - 1);
Vec.set env.tenv_queue 0 th_env
end;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue); assert (Vec.size env.trail_lim = Vec.size env.tenv_queue);
assert (env.qhead = Vec.size env.trail); assert (env.qhead = Vec.size env.trail);
() ()