From: Andrew Reynolds 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().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)