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 2ff45aef0009bb4cd78a078785851f01fa12a13c..3082377c74f727957f2baa6cc4b6d74b7f7adc86 100644 (file)
--- 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 05abda285a34d59281446e55c0f5b56c71389f79..f2f2c77f6d92763efb078f1246ce3c77124c9033 100644 (file)
--- 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 (file)
index 0000000..672c8cc
--- /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)