From 8c45a2ef94d68ceff7c0997e80d5b573895f2f69 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Fri, 13 Jun 2014 19:53:03 -0400
Subject: fixed BVMinisat bug due to not clearing seen properly

---
 src/prop/bvminisat/core/Solver.cc | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/prop/bvminisat')

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 8833eec78..e54c8d174 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -489,13 +489,12 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
     Var x = var(trail[i]);
     if (seen[x]) {
       if (reason(x) == CRef_Undef) {
-        // this is the case when p was a unit
-        if (x == var(p))
-          continue;
-        
-        assert (marker[x] == 2);
-        assert (level(x) > 0);
-        out_conflict.push(~trail[i]); 
+        // we skip p if was a learnt unit
+        if (x != var(p)) {
+          assert (marker[x] == 2);
+          assert (level(x) > 0);
+          out_conflict.push(~trail[i]);
+        }
       } else {
         Clause& c = ca[reason(x)];
         for (int j = 1; j < c.size(); j++)
@@ -504,6 +503,7 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
       }
       seen[x] = 0;
     }
+    assert (seen[x] == 0); 
   }
   assert (out_conflict.size()); 
 }
-- 
cgit v1.2.3