Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c84046570cde109b485febddf8d6340fcb9eaf18..c0365ab55f163b803f7ed81b95f448ba07d06568 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -141,7 +141,7 @@ static bool isClosed(Expr e, std::set<Expr>& free, std::hash_set<Expr, ExprHashF
   if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) {
     isClosed(e[1], free, closedCache);
     for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) {
-      free.erase((*i)[0]);
+      free.erase(*i);
     }
   } else if(e.getKind() == kind::BOUND_VARIABLE) {
     free.insert(e);