diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-12-10 17:17:00 -0300 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-10 14:17:00 -0600 |
| commit | d19c52821bb911413ff3dd4494c08a42a1db1e22 (patch) | |
| tree | aa91cb7bbc7aa66521b7bbfc528ab67394944616 /src/parser | |
| parent | ee5fed52332ec6baddc8ecd8f8e04a644990bf29 (diff) | |
Fix ufho issues (#3551)
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 73dea766a..151ecbfb4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1763,7 +1763,6 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) } } } - // Second phase: apply the arguments to the parse op ExprManager* em = getExprManager(); // handle special cases @@ -1833,6 +1832,19 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) } else if (isBuiltinOperator) { + if (!em->getOptions().getUfHo() + && (kind == kind::EQUAL || kind == kind::DISTINCT)) + { + // need --uf-ho if these operators are applied over function args + for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + { + if ((*i).getType().isFunction()) + { + parseError( + "Cannot apply equalty to functions unless --uf-ho is set."); + } + } + } if (args.size() > 2) { if (kind == kind::INTS_DIVISION || kind == kind::XOR |