1 files changed, 13 insertions, 3 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 86682f9a9..e964c020a 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -19,15 +19,22 @@
 grammar Smt;
 
 options {
-  language = 'C';                  // C output for antlr
-//  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
+  // C output for antlr
+  language = 'C';
+
+  // Skip the default error handling, just break with exceptions
+  // defaultErrorHandler = false;
+
+  // Only lookahead of <= k requested (disable for LL* parsing)
+  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // If you change this k, change it also in smt_input.cpp !
   k = 2;
 }
 
 @header {
 /**
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -49,11 +56,14 @@ options {
  * Otherwise, we have to let the lexer detect the encoding at runtime.
  */
 #define ANTLR3_INLINE_INPUT_ASCII
+
+#include "parser/antlr_tracing.h"
 }
 
 @parser::includes {
 #include "expr/command.h"
 #include "parser/parser.h"
+#include "parser/antlr_tracing.h"
 
 namespace CVC4 {
   class Expr;