Skip to content

Commit ce43b3e

Browse files
Move MAX_CONCRETE_STRING_SIZE definition to magic
1 parent d1b6da4 commit ce43b3e

File tree

3 files changed

+3
-2
lines changed

3 files changed

+3
-2
lines changed

src/solvers/refinement/string_refinement.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Author: Alberto Griggio, [email protected]
2828
#include <solvers/sat/satcheck.h>
2929
#include <solvers/refinement/string_constraint_instantiation.h>
3030
#include <unordered_set>
31+
#include <util/magic.h>
3132

3233
static bool is_valid_string_constraint(
3334
messaget::mstreamt &stream,

src/solvers/refinement/string_refinement.h

-2
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,6 @@ Author: Alberto Griggio, [email protected]
3131

3232
#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
3333
#define CHARACTER_FOR_UNKNOWN '?'
34-
// Limit the size of strings in traces to 64M chars to avoid memout
35-
#define MAX_CONCRETE_STRING_SIZE (1 << 26)
3634

3735
class string_refinementt final: public bv_refinementt
3836
{

src/util/magic.h

+2
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,7 @@
1010
const std::size_t CNF_DUMP_BLOCK_SIZE = 4096;
1111
const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
1212
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
13+
// Limit the size of strings in traces to 64M chars to avoid memout
14+
const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
1315

1416
#endif

0 commit comments

Comments
 (0)