From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 15 Feb 2018 23:34:54 +0000 (-0600)
Subject: Fix corner case for rewrite of mult by pow 2 (#1601)
X-Git-Tag: cvc5-1.0.0~5282
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98b9a45b8659e318bc529c223717f9f2fcd3b503;p=cvc5.git

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 169b28e34..d91067d1e 100644
--- 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 44691d1e2..eeeff7391 100644
--- 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
index 000000000..2f1697dbf
--- /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)