Fix invalid rewrite involving iand (#8026)

Fixes #8016.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 74d0b0d227f4e31ef8135e6749e2ba67027cf838..c5766594881877d23742116adbd894b54853acb6 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -749,8 +749,10 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
     }
     if (t[i].getConst<Rational>().getNumerator() == Integer(2).pow(bsize) - 1)
     {
-      // ((_ iand k) 111...1 y) ---> y
-      return RewriteResponse(REWRITE_DONE, t[i == 0 ? 1 : 0]);
+      // ((_ iand k) 111...1 y) ---> (mod y 2^k)
+      Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
+      Node ret = nm->mkNode(kind::INTS_MODULUS, t[1-i],  twok);
+      return RewriteResponse(REWRITE_AGAIN, ret);
     }
   }
   return RewriteResponse(REWRITE_DONE, t);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0085730e50b338636afe5380709b295f8c62ea82..c49d5004c8f65ca35a68f051b6cb70b09c76e6f9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1870,6 +1870,7 @@ set(regress_1_tests
   regress1/nl/issue5662-nl-tc.smt2
   regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/issue7924-sqrt-partial.smt2
+  regress1/nl/issue8016-iand-rewrite.smt2 
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2

diff --git a/test/regress/regress1/nl/issue8016-iand-rewrite.smt2 b/test/regress/regress1/nl/issue8016-iand-rewrite.smt2
new file mode 100644 (file)
index 0000000..ea797c9
--- /dev/null
+++ b/test/regress/regress1/nl/issue8016-iand-rewrite.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun v () Int)
+(assert (exists ((V Int)) (and (= 2 v) (= v ((_ iand 1) 1 v)))))
+(check-sat)