From 79fa41ee22465a31463e481e27299d29fd0b69e4 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 31 Aug 2010 13:59:43 +0000
Subject: [PATCH] Fix to the bvsolver. Some cases were missing when identifying
 monomials.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1008 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.cpp | 31 ++++++++++++++++++++++++++++++-
 unit_test/bvsolver.smt      | 15 +++++++++++++++
 unit_test/unit_test.sh      |  4 ++--
 3 files changed, 47 insertions(+), 3 deletions(-)
 create mode 100644 unit_test/bvsolver.smt

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 44d85d3..ef73f88 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -251,7 +251,35 @@ namespace BEEV
                 outmonom = monom;
                 chosen_symbol = true;
               }
+            else if (
+                !chosen_symbol
+                && monom.GetKind() == BVEXTRACT
+                && SYMBOL == monom[0].GetKind()
+                && BVCONST == monom[1].GetKind()
+                && zero == monom[2]
+                && !DoNotSolveThis(monom[0])
+                && count.single(monom[0])
+            )
+              {
+              outmonom = monom;
+              chosen_symbol = true;
+              }
+            else if (
+                       !chosen_symbol
+                       && monom.GetKind() == BVUMINUS
+                       && monom[0].GetKind() == BVEXTRACT
+                       && SYMBOL == monom[0][0].GetKind()
+                       && BVCONST == monom[0][1].GetKind()
+                       && zero == monom[0][2]
+                       && !DoNotSolveThis(monom[0][0])
+                       && count.single(monom[0][0])
+                   )
+                     {
+                     outmonom = monom;
+                     chosen_symbol = true;
+                     }
             else
+
               {
                 o.push_back(monom);
               }
@@ -833,7 +861,8 @@ namespace BEEV
        _bm->CreateNode(AND, o) : 
        o[0]) : 
       ASTTrue;
-    output = _bm->CreateNode(AND, output, evens);
+    if (evens != ASTTrue)
+      output = _bm->CreateNode(AND, output, evens);
 
     output = solveForAndOfXOR(output);
 
diff --git a/unit_test/bvsolver.smt b/unit_test/bvsolver.smt
new file mode 100644
index 0000000..1f391f1
--- /dev/null
+++ b/unit_test/bvsolver.smt
@@ -0,0 +1,15 @@
+(benchmark r
+  :status sat
+  :category { crafted }
+  :difficulty { 0 }
+  :logic QF_BV
+  :extrafuns ((x BitVec[3]))
+  :extrafuns ((y BitVec[3]))
+  :extrafuns ((z BitVec[3]))
+
+  :assumption (= (bvadd (bvadd (bvmul bv3[3] x) (bvmul bv4[3] y)) (bvmul bv2[3] z)) bv0[3])
+  :assumption (= (bvadd (bvadd (bvmul bv2[3] x) (bvmul bv2[3] y)) (bvmul bv0[3] z)) bv6[3])
+  :assumption (= (bvadd (bvadd (bvmul bv2[3] x) (bvmul bv4[3] y)) (bvmul bv2[3] z)) bv0[3])
+
+  :formula true
+)
diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
index cdd1cec..ba04404 100755
--- a/unit_test/unit_test.sh
+++ b/unit_test/unit_test.sh
@@ -5,12 +5,12 @@
 
 rm -f output_*.cnf
 
-files=`ls -1 -S *.smt2`
+files=`ls -1 -S *.smt2 *.smt`
 for f in $files; do
 	stp --output-CNF $f
 	cnf=`cat output_*.cnf  | grep -v "^c" | grep -v "^$" |  wc -l`
 	if [ $cnf -gt 3 ] ; then
-		echo --fail
+		echo --fail $f
 		exit 10
 	fi
 
-- 
2.47.3