From 3c2fc39e3b8b53466705bfd82818c442f6eb22e5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Oct 2013 11:05:23 -0500
Subject: [PATCH] Fix a bug in smt2 parser for quantified formulas with
 attributes, fixes bug 535

---
 src/parser/smt2/Smt2.g | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c84046570..c0365ab55 100644
--- 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);
-- 
2.30.2