diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 52539307f0f..7a080dd361a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -28,6 +28,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include static bool is_valid_string_constraint( messaget::mstreamt &stream, diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index f33c1bcf0b0..ec7892838ed 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -31,8 +31,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits::max() #define CHARACTER_FOR_UNKNOWN '?' -// Limit the size of strings in traces to 64M chars to avoid memout -#define MAX_CONCRETE_STRING_SIZE (1 << 26) class string_refinementt final: public bv_refinementt { diff --git a/src/util/magic.h b/src/util/magic.h index 48c72436e2d..3d1c2ed8d90 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -10,5 +10,7 @@ const std::size_t CNF_DUMP_BLOCK_SIZE = 4096; const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000; const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16; +// Limit the size of strings in traces to 64M chars to avoid memout +const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26; #endif