fixing a bug in the BV rewrite, off by one error when merging constants

3 files changed, 41 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 7cfb46835..dfc401616 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -33,6 +33,7 @@ bool RewriteRule<ConcatFlatten>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatFlatten>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
   std::vector<Node> processing_stack;
   processing_stack.push_back(node);
@@ -57,6 +58,9 @@ bool RewriteRule<ConcatExtractMerge>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
+
+  Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
+
   std::vector<Node> mergedExtracts;
 
   Node current = node[0];
@@ -115,6 +119,9 @@ bool RewriteRule<ConcatConstantMerge>::applies(Node node) {
 
 template<>
 Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
+
+  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
+
   std::vector<Node> mergedConstants;
   for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
     if (node[i].getKind() != kind::CONST_BITVECTOR) {
@@ -138,10 +145,12 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
       }
       // Add the new merged constant
       mergedConstants.push_back(utils::mkConst(current));
-      i = j + 1;
+      i = j;
     }
   }
 
+  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
+
   return utils::mkConcat(mergedConstants);
 }
 
@@ -158,6 +167,7 @@ bool RewriteRule<ExtractWhole>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractWhole>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
   return node[0];
 }
 
@@ -170,6 +180,7 @@ bool RewriteRule<ExtractConstant>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractConstant>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
   Node child = node[0];
   BitVector childValue = child.getConst<BitVector>();
   return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
@@ -177,6 +188,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) {
 
 template<>
 bool RewriteRule<ExtractConcat>::applies(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
   return true;
@@ -184,6 +196,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractConcat>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   int extract_high = utils::getExtractHigh(node);
   int extract_low = utils::getExtractLow(node);
 
@@ -216,6 +229,8 @@ bool RewriteRule<ExtractExtract>::applies(Node node) {
 
 template<>
 Node RewriteRule<ExtractExtract>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
+
   // x[i:j][k:l] ~>  x[k+j:l+j]
   Node child = node[0];
   unsigned k = utils::getExtractHigh(node);
@@ -228,6 +243,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) {
 
 template<>
 bool RewriteRule<FailEq>::applies(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
   if (node.getKind() != kind::EQUAL) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
   if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
@@ -247,6 +263,7 @@ bool RewriteRule<SimplifyEq>::applies(Node node) {
 
 template<>
 Node RewriteRule<SimplifyEq>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
   return utils::mkTrue();
 }
 
@@ -257,6 +274,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) {
 
 template<>
 Node RewriteRule<ReflexivityEq>::apply(Node node) {
+  Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
   return node[1].eqNode(node[0]);;
 }
 
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 25f977f3b..9182bfbc6 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -63,8 +63,9 @@ TESTS =	\
 	slice-18.smt \
 	slice-19.smt \
 	slice-20.smt \
-	ext_con_004_001_1024.smt 
-		
+	ext_con_004_001_1024.smt \
+	a78test0002.smt
+			
 EXTRA_DIST = $(TESTS)
 
 # synonyms for "check"
diff --git a/test/regress/regress0/bv/core/a78test0002.smt b/test/regress/regress0/bv/core/a78test0002.smt
new file mode 100644
index 000000000..28f6aea09
--- /dev/null
+++ b/test/regress/regress0/bv/core/a78test0002.smt
@@ -0,0 +1,19 @@
+(benchmark a78test0002.smt
+  :source {
+Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
+(vganesh@stanford.edu).  Translated into SMT-LIB format by Clark Barrett using
+CVC3.
+
+}
+  :status sat
+  :difficulty { 0 }
+  :category { industrial }
+  :logic QF_BV
+  :extrafuns ((r1 BitVec[16]))
+  :assumption
+(not (= r1 bv0[16]))
+  :assumption
+(not (not (= (concat bv0[16] r1) bv65535[32])))
+  :formula
+(not false)
+)