bv-to-int: fix translation of bvneg (#8437)

The translation of bvneg to integers did not match the comment documenting it, causing #8413 .
This PR fixes the issue and includes the test from #8413 as well as a simpler test.
Fixes #8413 .

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 875896cd45a0650c699f941e576335394e00d668..a0596b3b6800b1572b0e6ef35f845fac4b23d51e 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -255,6 +255,7 @@ Node IntBlaster::translateWithChildren(
   Assert(oldKind != kind::BITVECTOR_SREM);
   Assert(oldKind != kind::BITVECTOR_SMOD);
   Assert(oldKind != kind::BITVECTOR_XNOR);
+  Assert(oldKind != kind::BITVECTOR_NOR);
   Assert(oldKind != kind::BITVECTOR_NAND);
   Assert(oldKind != kind::BITVECTOR_SUB);
   Assert(oldKind != kind::BITVECTOR_REPEAT);
@@ -1080,8 +1081,8 @@ Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize)
 {
   // Based on Hacker's Delight section 2-2 equation a:
   // -x = ~x+1
-  Node p2 = pow2(bvsize);
-  return d_nm->mkNode(kind::SUB, p2, n);
+  Node bvNotNode = createBVNotNode(n, bvsize);
+  return createBVAddNode(bvNotNode, d_one, bvsize);
 }
 
 Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 000cbc3769a530826f62ca1c69a3fa692cc1fa1f..ac0ec5f052a752fd43efcac92cc2a429dcf3d9fb 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -278,6 +278,8 @@ set(regress_0_tests
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
+  regress0/bv/bv_to_int_issue_8413_1.smt2
+  regress0/bv/bv_to_int_issue_8413_2.smt2
   regress0/bv/bv_to_int_int1.smt2
   regress0/bv/bv_to_int_zext.smt2
   regress0/bv/bvcomp.cvc.smt2

diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2
new file mode 100644 (file)
index 0000000..48073ac
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
+; EXPECT: sat
+
+(set-logic QF_BV)
+
+(declare-fun zero () (_ BitVec 16))
+(declare-fun x () (_ BitVec 16))
+
+(assert (= zero (_ bv0 16)))
+(assert (= zero (bvneg x)))
+
+(check-sat)

diff --git a/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2
new file mode 100644 (file)
index 0000000..0dfa7a7
--- /dev/null
+++ b/test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=sum
+; EXPECT: sat
+
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 1))
+(assert (= (_ bv0 16) (bvsdiv ((_ zero_extend 8) ((_ zero_extend 7) a)) (bvnor (_ bv0 16) (_ bv0 16)))))
+(check-sat)