diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-01 11:05:23 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-01 11:05:30 -0500 |
| commit | 3c2fc39e3b8b53466705bfd82818c442f6eb22e5 (patch) | |
| tree | 13680d029dcaed5a0013b74d440ba3a5f8e79e71 | |
| parent | a747f01c1ee737bb8c4c1cc8ce355b79078d03d7 (diff) | |
Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 1 insertions, 1 deletions
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); |