From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 19:02:43 +0000 (-0400)
Subject: Fix SMT1 parser :extrasorts/:extrapreds.
X-Git-Tag: cvc5-1.0.0~6509^2~35
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6158285f826a33c4134def3e32b53e40483a173;p=cvc5.git

Fix SMT1 parser :extrasorts/:extrapreds.
---

diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index ae06ddc01..a885fe990 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -205,13 +205,13 @@ benchAttribute returns [CVC4::Command* smt_command = NULL]
       { ((CommandSequence*) smt_command)->addCommand(c); }
     )+ RPAREN_TOK
   | EXTRAPREDS_TOK LPAREN_TOK
-    ( { smt_command = new CommandSequence(); }
-      predicateDeclaration[c]
+    { smt_command = new CommandSequence(); }
+    ( predicateDeclaration[c]
       { ((CommandSequence*) smt_command)->addCommand(c); }
     )+ RPAREN_TOK
   | EXTRASORTS_TOK LPAREN_TOK
-    ( { smt_command = new CommandSequence(); }
-      sortDeclaration[c]
+    { smt_command = new CommandSequence(); }
+    ( sortDeclaration[c]
       { ((CommandSequence*) smt_command)->addCommand(c); }
     )+ RPAREN_TOK
   | NOTES_TOK STRING_LITERAL