Fix two multiply-by-constant corner cases for bv rewriter (#1562)

4 files changed, 32 insertions, 12 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index d17f20152..ad5b37a2d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -394,19 +394,22 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
   std::vector<Node> children;
   for (const TNode& current : node)
   {
-    if (current.getKind() == kind::CONST_BITVECTOR) {
-      BitVector value = current.getConst<BitVector>();
+    Node c = current;
+    if (c.getKind() == kind::BITVECTOR_NEG)
+    {
+      isNeg = !isNeg;
+      c = c[0];
+    }
+
+    if (c.getKind() == kind::CONST_BITVECTOR)
+    {
+      BitVector value = c.getConst<BitVector>();
       constant = constant * value;
       if(constant == BitVector(size, (unsigned) 0)) {
         return utils::mkConst(size, 0); 
       }
-    }
-    else if (current.getKind() == kind::BITVECTOR_NEG)
-    {
-      isNeg = !isNeg;
-      children.push_back(current[0]);
     } else {
-      children.push_back(current); 
+      children.push_back(c);
     }
   }
   BitVector oValue = BitVector(size, static_cast<unsigned>(1));
@@ -414,8 +417,7 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
 
   if (children.empty())
   {
-    Assert(!isNeg);
-    return utils::mkConst(constant);
+    return utils::mkConst(isNeg ? -constant : constant);
   }
 
   std::sort(children.begin(), children.end());
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 067440ee2..fb083c568 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -790,7 +790,15 @@ inline Node RewriteRule<MultPow2>::apply(TNode node)
     }
   }
 
-  Node a = utils::mkNode(kind::BITVECTOR_MULT, children);
+  Node a;
+  if (children.empty())
+  {
+    a = utils::mkOne(size);
+  }
+  else
+  {
+    a = utils::mkNode(kind::BITVECTOR_MULT, children);
+  }
 
   if (isNeg && size > 1)
   {
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 68a5f791c..912f6871d 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -105,7 +105,8 @@ SMT_TESTS = \
 	divtest_2_5.smt2 \
 	divtest_2_6.smt2 \
 	mul-neg-unsat.smt2 \
-	mul-negpow2.smt2
+	mul-negpow2.smt2 \
+	bvmul-pow2-only.smt2
 
 # This benchmark is currently disabled as it uses --check-proof
 # bench_38.delta.smt2
diff --git a/test/regress/regress0/bv/bvmul-pow2-only.smt2 b/test/regress/regress0/bv/bvmul-pow2-only.smt2
new file mode 100644
index 000000000..d4f085046
--- /dev/null
+++ b/test/regress/regress0/bv/bvmul-pow2-only.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 4))
+
+(assert (= x #b1000))
+
+(assert (= (bvmul (bvneg x) x) #b0000))
+(assert (= (bvmul (bvneg #b0100) #b0100) #b0000))
+(check-sat)