simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

[bugfix] semantic variables weren't reset when backtracking

Browse source
This commit is contained in:
Guillaume Bury 2015-01-13 18:02:06 +01:00
parent 017bcaad78
commit b05b21ac34
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcsolver.ml
View file

@ -259,7 +259,10 @@ module Make (E : Expr_intf.S)
env.tatoms_qhead <- env.qhead; env.tatoms_qhead <- env.qhead;
for c = env.qhead to Vec.size env.trail - 1 do for c = env.qhead to Vec.size env.trail - 1 do
Either.destruct (Vec.get env.trail c) Either.destruct (Vec.get env.trail c)
(fun a -> ()) (fun v ->
v.tag.assigned <- None;
v.level <- -1
)
(fun a -> (fun a ->
if a.var.level <= lvl then begin if a.var.level <= lvl then begin
Vec.set env.trail env.qhead (Either.mk_right a); Vec.set env.trail env.qhead (Either.mk_right a);