diff options
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c2f4675b1..bae02a5d2 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -2,9 +2,9 @@ /*! \file Tptp.g ** \verbatim ** Top contributors (to current version): - ** Francois Bobot, Morgan Deters, Andrew Reynolds + ** Haniel Barbosa, Francois Bobot, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; @@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist, PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector<api::Term> lchildren(++lhs.begin(), lhs.end()); rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs); - lhs = api::Term(lhs.getExpr().getOperator()); + lhs = api::Term(SOLVER, lhs.getExpr().getOperator()); } | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; |