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 a984fe16f19bb59dfb9e02d161a10a3222994cf2..719f2f38e62fd174a0164fc25870991d178afbf0 100644 (file)
--- 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());
     }
   }
 }