From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 5 Feb 2022 00:15:22 +0000 (-0600)
Subject: Fix another rewrite involving iand (#8054)
X-Git-Tag: cvc5-1.0.0~450
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d036ca9091767e31b41fc76afabd0cc6c451f153;p=cvc5.git

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 7d4bd4b83..abef4eec3 100644
--- 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 e1efca4f5..13c5e3094 100644
--- 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
index 000000000..c4d715090
--- /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)