Fix corner case for rewrite of mult by pow 2 (#1601)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 169b28e349f78eaf07b196c9629d68cc37e65d60..d91067d1ef9befd72952a6953abb869eb0983c4f 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -808,6 +808,10 @@ inline Node RewriteRule<MultPow2>::apply(TNode node)
       children.push_back(cn);
     }
   }
+  if (exponent >= size)
+  {
+    return utils::mkZero(size);
+  }
 
   Node a;
   if (children.empty())
@@ -823,7 +827,10 @@ inline Node RewriteRule<MultPow2>::apply(TNode node)
   {
     a = nm->mkNode(kind::BITVECTOR_NEG, a);
   }
-
+  if (exponent == 0)
+  {
+    return a;
+  }
   Node extract = utils::mkExtract(a, size - exponent - 1, 0);
   Node zeros = utils::mkConst(exponent, 0);
   return utils::mkConcat(extract, zeros); 

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 44691d1e29dd2d0b7c1334407c59c0b9016c63e2..eeeff73919f61662381602cf3c7f4f408056fa1c 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -101,7 +101,8 @@ SMT_TESTS = \
        divtest_2_6.smt2 \
        mul-neg-unsat.smt2 \
        mul-negpow2.smt2 \
-       bvmul-pow2-only.smt2
+       bvmul-pow2-only.smt2 \
+       mult-pow2-negative.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = bvsimple.cvc sizecheck.cvc

diff --git a/test/regress/regress0/bv/mult-pow2-negative.smt2 b/test/regress/regress0/bv/mult-pow2-negative.smt2
new file mode 100644 (file)
index 0000000..2f1697d
--- /dev/null
+++ b/test/regress/regress0/bv/mult-pow2-negative.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 4))
+(assert (not (= (bvmul (bvneg (bvmul #b1111 #b1111)) #b1111) x)))
+(check-sat)