From b62abe729cd029af9ab3e27f7f1a7cde28bb4b08 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 19 Sep 2017 13:17:04 -0700 Subject: [PATCH] Removing a potentially invalid comparison in the TPTP parser. (#1091) --- src/parser/tptp/tptp.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index a984fe16f..719f2f38e 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -213,14 +213,20 @@ void Tptp::checkLetBinding(std::vector& bvlist, Expr lhs, Expr rhs, bool f std::sort(v.begin(), v.end()); std::sort(bvlist.begin(), bvlist.end()); // ensure all let-bound variables appear on the LHS, and appear only once - for(size_t i = 0; i < bvlist.size(); ++i) { - std::vector::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]); - if(found == v.end() || *found != bvlist[i]) { - parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'"); + for (size_t i = 0; i < bvlist.size(); ++i) { + std::vector::const_iterator found = + std::lower_bound(v.begin(), v.end(), bvlist[i]); + if (found == v.end() || *found != bvlist[i]) { + parseError( + "malformed let: LHS must make use of all quantified variables, " + "missing `" + + bvlist[i].toString() + "'"); } + assert(found != v.end()); std::vector::const_iterator found2 = found + 1; - if(found2 != v.end() && *found2 == *found) { - parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString()); + if (found2 != v.end() && *found2 == *found) { + parseError("malformed let: LHS cannot use same bound variable twice: " + + (*found).toString()); } } } -- 2.30.2