summaryrefslogtreecommitdiff
path: root/src/parser/cvc/Cvc.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r--src/parser/cvc/Cvc.g5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2988ae4ef..21f82f638 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -430,12 +430,15 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
* the lexer headers for two grammars AND (b) uses the token symbol definitions. */
#pragma GCC system_header
+#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
/* This improves performance by ~10 percent on big inputs.
* This option is only valid if we know the input is ASCII (or some 8-bit encoding).
* If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
* Otherwise, we have to let the lexer detect the encoding at runtime.
*/
-#define ANTLR3_INLINE_INPUT_ASCII
+# define ANTLR3_INLINE_INPUT_ASCII
+# define ANTLR3_INLINE_INPUT_8BIT
+#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
#include "parser/antlr_tracing.h"
#include "util/integer.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback