diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 1355cffa8..5041d0da3 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -2311,10 +2311,10 @@ static void display_smt2(std::ostream& out) {
         asms.push_back(fmls.m_formulas[i]);
 
     for (size_t i = 0; i < asms.size(); ++i) {
-        z3::expr fml = asms[i];
+        z3::expr fml = asms[(unsigned)i];
         if (fml.is_and()) {
             z3::expr arg0 = fml.arg(0);
-            asms.set(i, arg0);
+            asms.set((unsigned)i, arg0);
             for (unsigned j = 1; j < fml.num_args(); ++j)
                 asms.push_back(fml.arg(j));
             --i;
@@ -2323,7 +2323,7 @@ static void display_smt2(std::ostream& out) {
     
     Z3_ast* assumptions = new Z3_ast[asms.size()];
     for (size_t i = 0; i < asms.size(); ++i) 
-        assumptions[i] = asms[i];        
+        assumptions[i] = asms[(unsigned)i];        
     Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB_FULL);
     Z3_string s = 
         Z3_benchmark_to_smtlib_string(
diff --git a/examples/tptp/tptp5.lex.cpp b/examples/tptp/tptp5.lex.cpp
index ece0fbf86..fb6ccfa51 100644
--- a/examples/tptp/tptp5.lex.cpp
+++ b/examples/tptp/tptp5.lex.cpp
@@ -147,7 +147,7 @@ typedef unsigned int flex_uint32_t;
 
 /* Size of default input buffer. */
 #ifndef YY_BUF_SIZE
-#define YY_BUF_SIZE 16384
+#define YY_BUF_SIZE 8*16384
 #endif
 
 /* The state buf must be large enough to hold one state per character in the main buffer.
@@ -648,7 +648,7 @@ static int yy_prev_more_offset = 0;
 	yyleng -= (yy_more_offset); \
 	}
 #ifndef YYLMAX
-#define YYLMAX 8192
+#define YYLMAX 2*8*8192
 #endif
 
 char yytext[YYLMAX];
@@ -1877,6 +1877,7 @@ static int yy_get_next_buffer (void)
 		while ( num_to_read <= 0 )
 			{ /* Not enough room in the buffer - grow it. */
 
+            printf("%zu %d %zu\n", YY_CURRENT_BUFFER_LVALUE->yy_buf_size, number_to_move, num_to_read);
 			YY_FATAL_ERROR(
 "input buffer overflow, can't enlarge buffer because scanner uses REJECT" );