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

2 files changed, 21 insertions, 11 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)
   {