From 60973169af7ad8653436fc6497e13e25897ed578 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 16 Dec 2021 17:52:09 +0200 Subject: [PATCH] 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 --- src/preprocessing/passes/int_to_bv.cpp | 6 ++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/proj-issue-348.smt2 | 8 ++++++++ 3 files changed, 15 insertions(+) create mode 100644 test/regress/regress0/nl/proj-issue-348.smt2 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) -- 2.30.2