diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 156f2e1e6..764e83361 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -22,6 +22,7 @@ #include "api/cpp/cvc5.h" #include "base/check.h" #include "options/options.h" +#include "options/options_public.h" #include "parser/parser.h" #include "smt/command.h" @@ -315,7 +316,8 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // Second phase: apply parse op to the arguments if (isBuiltinKind) { - if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!options::getUfHo(opts) + && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); @@ -362,7 +364,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!opts.getUfHo()) + if (!options::getUfHo(opts)) { parseError("Cannot partially apply functions unless --uf-ho is set."); } |