From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 26 Aug 2021 00:50:53 +0000 (-0700)
Subject: int2bv: Fix conversion of signed bit-vector values. (#7061)
X-Git-Tag: cvc5-1.0.0~1335
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a81064b538382670f25c87f138961f12def7880a;p=cvc5.git

int2bv: Fix conversion of signed bit-vector values. (#7061)

This commit fixes the conversion of signed bit-vector values to integers in the int-to-bv preprocessing pass.
---

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 8c18ccf54..41d52d1ae 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -217,8 +217,20 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
           result = sm->mkDummySkolem("__intToBV_var",
                                      nm->mkBitVectorType(size),
                                      "Variable introduced in intToBV pass");
-          Node bv2nat = nm->mkNode(kind::BITVECTOR_TO_NAT, result);
-          d_preprocContext->addSubstitution(current, bv2nat);
+          /**
+           * Correctly convert signed/unsigned BV values to Integers as follows
+           * x < 0 ? -nat(-x) : nat(x)
+           * where x refers to the bit-vector term `result`.
+           */
+          BitVector bvzero(size, Integer(0));
+          Node negResult = nm->mkNode(kind::BITVECTOR_TO_NAT,
+                                      nm->mkNode(kind::BITVECTOR_NEG, result));
+          Node bv2int = nm->mkNode(
+              kind::ITE,
+              nm->mkNode(kind::BITVECTOR_SLT, result, nm->mkConst(bvzero)),
+              nm->mkNode(kind::UMINUS, negResult),
+              nm->mkNode(kind::BITVECTOR_TO_NAT, result));
+          d_preprocContext->addSubstitution(current, bv2int);
         }
       }
       else if (current.isConst())
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ce047c877..ec6d04c1d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -420,6 +420,7 @@ set(regress_0_tests
   regress0/bv/inequality05.smt2
   regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/int_to_bv_model.smt2
+  regress0/bv/int_to_bv_model2.smt2
   regress0/bv/issue-4075.smt2
   regress0/bv/issue-4076.smt2
   regress0/bv/issue-4130.smt2
diff --git a/test/regress/regress0/bv/int_to_bv_model2.smt2 b/test/regress/regress0/bv/int_to_bv_model2.smt2
new file mode 100644
index 000000000..d4ad9695f
--- /dev/null
+++ b/test/regress/regress0/bv/int_to_bv_model2.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --solve-int-as-bv=5 --check-models
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-const x Int)
+(assert (< x 0))
+(check-sat)