Fix SMT1 parser :extrasorts/:extrapreds.
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 22 Aug 2014 19:02:43 +0000 (15:02 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Fri, 22 Aug 2014 19:03:41 +0000 (15:03 -0400)
src/parser/smt1/Smt1.g

index ae06ddc010b16aadf8b3a734f23ffcb7f774ea19..a885fe9905a148daaa145be787c58f7660f45f5a 100644 (file)
@@ -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