diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp index 76f939acfd..b5f5a2ae53 100644 --- a/src/util/stackinfo.cpp +++ b/src/util/stackinfo.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "util/exception.h" #if !defined(LEAN_USE_SPLIT_STACK) - #if defined(LEAN_WINDOWS) // no extra included needed so far #elif defined(__APPLE__) @@ -21,8 +20,6 @@ Author: Leonardo de Moura #include // NOLINT #endif -#define LEAN_MIN_STACK_SPACE 128*1024 // 128 Kb - namespace lean { void throw_get_stack_size_failed() { throw exception("failed to retrieve thread stack size"); @@ -92,7 +89,7 @@ size_t get_available_stack_size() { void check_stack(char const * component_name) { if (!g_stack_info_init) save_stack_info(false); - if (get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size) + if (get_used_stack_size() + LEAN_STACK_BUFFER_SPACE > g_stack_size) throw stack_space_exception(component_name); } } diff --git a/src/util/thread.cpp b/src/util/thread.cpp index 3034d5e1c5..d289209697 100644 --- a/src/util/thread.cpp +++ b/src/util/thread.cpp @@ -20,7 +20,7 @@ namespace lean { size_t lthread::m_thread_stack_size = LEAN_DEFAULT_THREAD_STACK_SIZE; void lthread::set_thread_stack_size(size_t sz) { - m_thread_stack_size = sz; + m_thread_stack_size = sz + LEAN_STACK_BUFFER_SPACE; } size_t lthread::get_thread_stack_size() { diff --git a/src/util/thread.h b/src/util/thread.h index ecb342aa02..2c88848aad 100644 --- a/src/util/thread.h +++ b/src/util/thread.h @@ -7,6 +7,10 @@ Author: Leonardo de Moura #pragma once #include +#ifndef LEAN_STACK_BUFFER_SPACE +#define LEAN_STACK_BUFFER_SPACE 128*1024 // 128 Kb +#endif + #if defined(LEAN_MULTI_THREAD) #include #include