[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 c85e57b65b782f267a39c1cc7d9cb7269910bbb5..9b755a23054d8e0dcd381b1c42461b9b7ada9287 100644 (file)
--- 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 984e0e8a78ab13bf7c2f47fc8e0597d7f4856892..95fe01c0f2301afc74af8936829e04082967ca75 100644 (file)
--- 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 (file)
index 0000000..1512eae
--- /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)