From b05b21ac34878407ffc6e8a71fcf80cf4644c3f1 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 13 Jan 2015 18:02:06 +0100
Subject: [PATCH] [bugfix] semantic variables weren't reset when backtracking

---
 solver/mcsolver.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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