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.

1 files changed, 7 insertions, 3 deletions

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index f50cecd1b..1c77f6f54 100644
--- 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())
         {