From ebf837cd9401828603ccc949aa1f6ead74572a5b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Jun 2012 06:04:21 +0000
Subject: [PATCH] fixed smt version 1 parser for quantifiers

---
 src/parser/smt/Smt.g | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 9f1f458c9..d44f7abcb 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -225,6 +225,7 @@ annotatedFormula[CVC4::Expr& expr]
   Kind kind;
   std::string name;
   std::vector<Expr> args; /* = getExprVector(); */
+  std::vector<Expr> args2;
   Expr op; /* Operator expression FIXME: move away kill it */
 }
   : /* a built-in operator application */
@@ -255,8 +256,9 @@ annotatedFormula[CVC4::Expr& expr]
       { args.push_back(PARSER_STATE->mkVar(name, t)); }
     )+
     annotatedFormula[expr] RPAREN_TOK
-    { args.push_back(expr);
-      expr = MK_EXPR(kind, args);
+    { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
+      args2.push_back(expr);
+      expr = MK_EXPR(kind, args2);
       PARSER_STATE->popScope();
     }
 
-- 
2.30.2