mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

handle larger buffers

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-13 14:11:51 -07:00
parent 6b32aaed10
commit 0d3c29a250
2 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
examples/tptp/tptp5.cpp
View file

@ -2311,10 +2311,10 @@ static void display_smt2(std::ostream& out) {
asms.push_back(fmls.m_formulas[i]); asms.push_back(fmls.m_formulas[i]);
for (size_t i = 0; i < asms.size(); ++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()) { if (fml.is_and()) {
z3::expr arg0 = fml.arg(0); z3::expr arg0 = fml.arg(0);
asms.set(i, arg0); asms.set((unsigned)i, arg0);
for (unsigned j = 1; j < fml.num_args(); ++j) for (unsigned j = 1; j < fml.num_args(); ++j)
asms.push_back(fml.arg(j)); asms.push_back(fml.arg(j));
--i; --i;
@ -2323,7 +2323,7 @@ static void display_smt2(std::ostream& out) {
Z3_ast* assumptions = new Z3_ast[asms.size()]; Z3_ast* assumptions = new Z3_ast[asms.size()];
for (size_t i = 0; i < asms.size(); ++i) 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_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB_FULL);
Z3_string s = Z3_string s =
Z3_benchmark_to_smtlib_string( Z3_benchmark_to_smtlib_string(

5
examples/tptp/tptp5.lex.cpp
View file

@ -147,7 +147,7 @@ typedef unsigned int flex_uint32_t;
/* Size of default input buffer. */ /* Size of default input buffer. */
#ifndef YY_BUF_SIZE #ifndef YY_BUF_SIZE
#define YY_BUF_SIZE 16384 #define YY_BUF_SIZE 8*16384
#endif #endif
/* The state buf must be large enough to hold one state per character in the main buffer. /* 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); \ yyleng -= (yy_more_offset); \
} }
#ifndef YYLMAX #ifndef YYLMAX
#define YYLMAX 8192 #define YYLMAX 2*8*8192
#endif #endif
char yytext[YYLMAX]; char yytext[YYLMAX];
@ -1877,6 +1877,7 @@ static int yy_get_next_buffer (void)
while ( num_to_read <= 0 ) while ( num_to_read <= 0 )
{ /* Not enough room in the buffer - grow it. */ { /* 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( YY_FATAL_ERROR(
"input buffer overflow, can't enlarge buffer because scanner uses REJECT" ); "input buffer overflow, can't enlarge buffer because scanner uses REJECT" );