diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bf4e489bb..a7eb218af 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -642,6 +642,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { addOperator(api::SELECT, "select"); addOperator(api::STORE, "store"); + addOperator(api::EQ_RANGE, "eqrange"); } if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { @@ -1824,6 +1825,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } + if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") + { + parseError( + "eqrange predicate requires option --arrays-exp to be enabled."); + } api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; |