From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Oct 2013 16:05:23 +0000 (-0500)
Subject: Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535
X-Git-Tag: cvc5-1.0.0~7286^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c2fc39e3b8b53466705bfd82818c442f6eb22e5;p=cvc5.git

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 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);