diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index aba409109..46a2e2c59 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -332,8 +332,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const bool Smt2::isHoEnabled() const { - return getLogic().isHigherOrder() - && d_solver->getExprManager()->getOptions().getUfHo(); + return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo(); } bool Smt2::logicIsSet() { @@ -999,7 +998,7 @@ void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt, InputLanguage Smt2::getLanguage() const { - return d_solver->getExprManager()->getOptions().getInputLanguage(); + return d_solver->getOptions().getInputLanguage(); } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) @@ -1162,7 +1161,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } } // Second phase: apply the arguments to the parse op - const Options& opts = d_solver->getExprManager()->getOptions(); + const Options& opts = d_solver->getOptions(); // handle special cases if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { |