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

---
 src/prop/bvminisat/core/Solver.cc             | 14 +++++------
 test/regress/regress0/bv/Makefile.am          |  4 +++-
 .../regress/regress0/bv/unsound1-reduced.smt2 | 11 +++++++++
 test/regress/regress0/bv/unsound1.smt2        | 23 +++++++++++++++++++
 4 files changed, 44 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress0/bv/unsound1-reduced.smt2
 create mode 100644 test/regress/regress0/bv/unsound1.smt2

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()); 
 }
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 4c2b1c773..fa9ee41a1 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -91,7 +91,9 @@ SMT_TESTS = \
 	fuzz40.smt \
 	fuzz41.smt \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \
-	smtcompbug.smt
+	smtcompbug.smt \
+	unsound1.smt2 \
+	unsound1-reduced.smt2
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = divtest.smt2
diff --git a/test/regress/regress0/bv/unsound1-reduced.smt2 b/test/regress/regress0/bv/unsound1-reduced.smt2
new file mode 100644
index 000000000..94858166d
--- /dev/null
+++ b/test/regress/regress0/bv/unsound1-reduced.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(assert
+	(xor
+		(bvslt (_ bv0 5)
+		       (bvlshr (bvadd (_ bv5 5) ((_ sign_extend 3) v0)) ((_ sign_extend 3) v0)))
+	     	 (bvult (_ bv5 5)
+	     	        (bvlshr (bvadd (_ bv5 5) ((_ sign_extend 3) v0)) ((_ sign_extend 3) v0)))))
+(check-sat)
+
diff --git a/test/regress/regress0/bv/unsound1.smt2 b/test/regress/regress0/bv/unsound1.smt2
new file mode 100644
index 000000000..60e764537
--- /dev/null
+++ b/test/regress/regress0/bv/unsound1.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 4))
+(assert (let ((e1(_ bv0 1)))
+(let ((e2(_ bv11134 16)))
+(let ((e3 (bvadd e2 ((_ sign_extend 12) v0))))
+(let ((e4 (ite (= e2 ((_ sign_extend 12) v0)) (_ bv1 1) (_ bv0 1))))
+(let ((e5 (bvlshr e3 ((_ sign_extend 12) v0))))
+(let ((e6 (bvxnor e2 ((_ zero_extend 12) v0))))
+(let ((e7 (ite (bvult ((_ sign_extend 15) e1) e2) (_ bv1 1) (_ bv0 1))))
+(let ((e8 (bvugt e7 e1)))
+(let ((e9 (bvule ((_ sign_extend 3) e7) v0)))
+(let ((e10 (bvsgt e5 ((_ zero_extend 12) v0))))
+(let ((e11 (= e6 e3)))
+(let ((e12 (bvslt ((_ zero_extend 15) e4) e5)))
+(let ((e13 (bvugt e5 e2)))
+(let ((e14 (ite e10 e8 e10)))
+(let ((e15 (xor e13 e11)))
+(let ((e16 (xor e14 e15)))
+(let ((e17 (ite e9 e12 e16)))
+e17
+))))))))))))))))))
+(check-sat)
-- 
2.30.2