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

Removed assertion

Browse source 
Long explanation: when backtracking to level 0,
while already being at level 0, very strange
things might happen, most notably there might still
be facts left to propagate...
This commit is contained in:
Guillaume Bury 2015-11-18 17:43:26 +01:00
parent 6567d32900
commit 28f32de24c
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
solver/internal.ml
View file

@ -317,7 +317,6 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl);
end;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue);
assert (env.qhead = Vec.size env.trail);
()
let report_unsat ({atoms=atoms} as confl) =