From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 16 Dec 2021 15:52:09 +0000 (+0200)
Subject: int-to-bv: fail if one of the arguments has type real (#7810)
X-Git-Tag: cvc5-1.0.0~656
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60973169af7ad8653436fc6497e13e25897ed578;p=cvc5.git

int-to-bv: fail if one of the arguments has type real (#7810)

This PR generates a failure in int-to-bv in case a real argument is detected as a child of an arithmetic operation.
fixes cvc5/cvc5-projects#348 .

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com
---

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 2ff45aef0..3082377c7 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -117,6 +117,12 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
   for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
            [&cache](TNode nn) { return cache.count(nn) > 0; }))
   {
+    TypeNode tn = current.getType();
+    if (tn.isReal() && !tn.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          current, string("Cannot translate to BV: ") + current.toString());
+    }
     if (current.getNumChildren() > 0)
     {
       // Not a leaf
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 05abda285..f2f2c77f6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -775,6 +775,7 @@ set(regress_0_tests
   regress0/nl/pow2-native-3.smt2
   regress0/nl/pow2-pow.smt2
   regress0/nl/pow2-pow-isabelle.smt2
+  regress0/nl/proj-issue-348.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
   regress0/nl/sin-cos-346-b-chunk-0169.smt2
diff --git a/test/regress/regress0/nl/proj-issue-348.smt2 b/test/regress/regress0/nl/proj-issue-348.smt2
new file mode 100644
index 000000000..672c8cc4c
--- /dev/null
+++ b/test/regress/regress0/nl/proj-issue-348.smt2
@@ -0,0 +1,8 @@
+; EXIT: 1
+; EXPECT: Cannot translate to BV
+; SCRUBBER: sed -n "s/.*\(Cannot translate to BV\).*/\1/p"
+(set-logic ALL)
+(set-option :solve-int-as-bv 1)
+(declare-const x Real)
+(assert (>= 0.0 x))
+(check-sat)