diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/real_to_int.cpp | 10 |
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()) { |