From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 1 Mar 2022 09:07:56 +0000 (-0800)
Subject: [BV] Fix rewriter policy for `bvneg` (#8196)
X-Git-Tag: cvc5-1.0.0~355
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f67de1dc1492f12e14d46316dcdd680d753b58c;p=cvc5.git

[BV] Fix rewriter policy for `bvneg` (#8196)

Our rewriter was returning `REWRITE_DONE` prematurely for `bvneg`. This
commit makes the status returned more conservative.
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index c85e57b65..9b755a230 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -486,7 +486,11 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
     }
   }
 
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  // There are cases where we need to rewrite the resulting term again. For
+  // example, if we rewrite (bvneg (bvneg (bvneg #b0))) to (bvneg #b0) then we
+  // have to rewrite again.
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE,
+                         resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 984e0e8a7..95fe01c0f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -446,6 +446,7 @@ set(regress_0_tests
   regress0/bv/issue-4130.smt2
   regress0/bv/issue3621.smt2
   regress0/bv/issue5396.smt2
+  regress0/bv/issue8159-1-rewrite-bvneg.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
diff --git a/test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2 b/test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2
new file mode 100644
index 000000000..1512eaedb
--- /dev/null
+++ b/test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --incremental
+(set-logic QF_BV)
+(assert (= (_ bv1 1) (bvsmod (_ bv0 1) (bvneg (bvneg (_ bv0 1))))))
+(push)
+(set-info :status unsat)
+(check-sat)