diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-12 16:13:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-12 16:13:27 -0500 |
commit | dd84f87edba9b0cde271fe7000208c5f8f97b890 (patch) | |
tree | 4cb6f0c00a45250fa575d13f49c502ec01026b89 /src/preprocessing | |
parent | 920343a4a5586297dd98305b83785207025083b8 (diff) |
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.
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()) { |