Do not allow quantifiers over real variables in real to int pass. (#4049)

With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index f50cecd1bec3b1f5f76827a20a5c2422c3079de3..1c77f6f54bb1bf95ef5b751b708759e73dff2b00 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -115,7 +115,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
                 {
                   throw TypeCheckingException(
                       v.toExpr(),
-                      string("Cannot translate to Int: ") + v.toString());
+                      std::string("Cannot translate to Int: ") + v.toString());
                 }
               }
             }
@@ -166,8 +166,12 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
       {
         if (n.getKind() == kind::BOUND_VARIABLE)
         {
-          // special case for bound variables (must call mkBoundVar)
-          ret = nm->mkBoundVar(nm->integerType());
+          // cannot change the type of quantified variables, since this leads
+          // to incompleteness.
+          throw TypeCheckingException(
+              n.toExpr(),
+              std::string("Cannot translate bound variable to Int: ")
+                  + n.toString());
         }
         else if (n.isVar())
         {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index de2091ef6f156ee59bb94a56954fb8914fd88552..c23ed07ee315cb82d8236b28ddbedfa9854e81df 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -690,7 +690,6 @@ set(regress_0_tests
   regress0/push-pop/incremental-subst-bug.cvc
   regress0/push-pop/issue1986.smt2
   regress0/push-pop/issue2137.min.smt2
-  regress0/push-pop/issue3915-real-as-int.smt2
   regress0/push-pop/quant-fun-proc-unfd.smt2
   regress0/push-pop/real-as-int-incremental.smt2
   regress0/push-pop/simple_unsat_cores.smt2

diff --git a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2 b/test/regress/regress0/push-pop/issue3915-real-as-int.smt2
deleted file mode 100644 (file)
index ad6ba3b..0000000
--- a/test/regress/regress0/push-pop/issue3915-real-as-int.smt2
+++ /dev/null
@@ -1,33 +0,0 @@
-; COMMAND-LINE: --incremental --check-models --solve-real-as-int\r
-; EXPECT: sat\r
-(set-logic UFNIA)\r
-(set-option :incremental true)\r
-(set-option :check-models true)\r
-(set-option :solve-real-as-int true)\r
-(declare-const v0 Bool)\r
-(declare-const v1 Bool)\r
-(declare-const v2 Bool)\r
-(declare-const v3 Bool)\r
-(declare-const v4 Bool)\r
-(declare-const v5 Bool)\r
-(declare-const v6 Bool)\r
-(declare-const v7 Bool)\r
-(declare-const v8 Bool)\r
-(declare-const v9 Bool)\r
-(declare-const v10 Bool)\r
-(declare-const v11 Bool)\r
-(declare-const v12 Bool)\r
-(declare-const v13 Bool)\r
-(declare-const v14 Bool)\r
-(declare-const i1 Int)\r
-(assert (forall ((q0 Int) (q1 Int) (q2 Int) (q3 Bool)) (=> (= v7 q3 v7 q3 v0 q3 q3 q3 q3 v3) (> q0 59))))\r
-(push 1)\r
-(declare-const v15 Bool)\r
-(declare-sort S0 0)\r
-(declare-sort S1 0)\r
-(declare-const i2 Int)\r
-(assert v13)\r
-(push 1)\r
-(declare-const S1-0 S1)\r
-(assert (forall ((q4 Int)) (not (distinct q4 q4))))\r
-(check-sat)\r