From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Jun 2012 06:04:21 +0000 (+0000)
Subject: fixed smt version 1 parser for quantifiers
X-Git-Tag: cvc5-1.0.0~7976
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ebf837cd9401828603ccc949aa1f6ead74572a5b;p=cvc5.git

fixed smt version 1 parser for quantifiers
---

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