Fix another rewrite involving iand (#8054)

Fixes #8052.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 7d4bd4b8372fc893785705780194b7924a9a1e84..abef4eec33de48f706ec80d2819bd20cf2cb5101 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -732,8 +732,10 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
   }
   else if (t[0] == t[1])
   {
-    // ((_ iand k) x x) ---> x
-    return RewriteResponse(REWRITE_DONE, t[0]);
+    // ((_ iand k) x x) ---> (mod x 2^k)
+    Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
+    Node ret = nm->mkNode(kind::INTS_MODULUS, t[0],  twok);
+    return RewriteResponse(REWRITE_AGAIN, ret);
   }
   // simplifications involving constants
   for (unsigned i = 0; i < 2; i++)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e1efca4f50f3c1ea5a5787739e6b540e013701b6..13c5e3094aff5a839c6981e380f9b93b0d614e02 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1880,6 +1880,7 @@ set(regress_1_tests
   regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/issue7924-sqrt-partial.smt2
   regress1/nl/issue8016-iand-rewrite.smt2 
+  regress1/nl/issue8052-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/issue8052-iand-rewrite.smt2 b/test/regress/regress1/nl/issue8052-iand-rewrite.smt2
new file mode 100644 (file)
index 0000000..c4d7150
--- /dev/null
+++ b/test/regress/regress1/nl/issue8052-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) v v)))))
+(check-sat)