3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00

Prevent Z3_solver_reset abort after memory_max_size OOM by making reset memory-limit-safe (#10254)

`memory_max_size` OOMs were recoverable at `check_sat` time
(`Z3_L_UNDEF` + error handler), but `Z3_solver_reset` could still
terminate the process with an uncaught `out_of_memory_error`. This
change keeps reset on the C API error-reporting path instead of letting
teardown allocations trip the same hard limit.

- **Reset path hardening**
- `Z3_solver_reset` now performs solver teardown under a temporary
suspension of the global memory cap, then restores the previous cap
afterward.
- This avoids aborts when allocator accounting is still above
`memory_max_size` at reset time.

- **Memory manager support**
- Added `memory::get_max_size()` to snapshot/restore the active cap
precisely.

- **Regression coverage**
- Extended `src/test/memory.cpp` with a focused scenario that trips
`Z3_MEMOUT_FAIL` and then calls `Z3_solver_reset` under a non-throwing
error handler, covering the previously aborting recovery path.

```cpp
struct scoped_memory_limit_reset {
    size_t m_prev_max;
    scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
        memory::set_max_size(0);
    }
    ~scoped_memory_limit_reset() {
        memory::set_max_size(m_prev_max);
    }
} scoped_max_memory;
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10250

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-27 12:46:32 -07:00 committed by GitHub
parent ad4896c3e0
commit aa0ebc6efc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 57 additions and 1 deletions

View file

@ -22,6 +22,7 @@ Revision History:
#include "util/file_path.h"
#include "util/scoped_timer.h"
#include "util/file_path.h"
#include "util/memory_manager.h"
#include "ast/ast_pp.h"
#include "api/z3.h"
#include "api/api_log_macros.h"
@ -514,6 +515,15 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_reset(c, s);
RESET_ERROR_CODE();
struct scoped_memory_limit_reset {
size_t m_prev_max;
scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
memory::set_max_size(0);
}
~scoped_memory_limit_reset() {
memory::set_max_size(m_prev_max);
}
} scoped_max_memory;
to_solver(s)->m_solver = nullptr;
to_solver(s)->m_cmd_context = nullptr;
if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset();