From: Tim King <taking@cs.nyu.edu>
Date: Tue, 19 Sep 2017 20:17:04 +0000 (-0700)
Subject: Removing a potentially invalid comparison in the TPTP parser. (#1091)
X-Git-Tag: cvc5-1.0.0~5628
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b62abe729cd029af9ab3e27f7f1a7cde28bb4b08;p=cvc5.git

Removing a potentially invalid comparison in the TPTP parser. (#1091)
---

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<Expr>& 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<CVC4::Expr>::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<CVC4::Expr>::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<CVC4::Expr>::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());
     }
   }
 }