diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 71a3e4bee..bf699ae3c 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -326,7 +326,9 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args) || kind == kind::LEQ || kind == kind::GEQ) { /* "chainable", but CVC4 internally only supports 2 args */ - return em->mkExpr(em->mkConst(Chain(kind)), args); + api::Term ret = + mkChain(intToExtKind(kind), api::exprVectorToTerms(args)); + return ret.getExpr(); } } |