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

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

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)

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

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)

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)