From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Feb 2022 21:21:24 +0000 (-0600)
Subject: Fix invalid rewrite involving iand (#8026)
X-Git-Tag: cvc5-1.0.0~473
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d4b79e59f318ffa50d816411d649420c10a2013;p=cvc5.git

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 74d0b0d22..c57665948 100644
--- 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 0085730e5..c49d5004c 100644
--- 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
index 000000000..ea797c983
--- /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)