mirror of
https://github.com/Z3Prover/z3
synced 2026-06-20 15:40:37 +00:00
e4e5d57cf6
## Summary Fix a use-after-free in `func_interp::compress()`. When a function interpretation had previously grown large enough to allocate `m_entry_table`, `compress()` could deallocate entries whose result matched the else-case but leave the hash table intact. Later `get_entry()` lookups could then return freed `func_entry*` values, which showed up during model checking as a corrupted expression result from `model_evaluator`. ## Root cause `func_interp::compress()` compacted `m_entries` and freed removed entries, but it did not rebuild or clear `m_entry_table`. This left stale pointers in the lookup table whenever: - the table had already been allocated on a larger interpretation, and - compression removed some entries. In the reported case, model evaluation rewrote `stack_s!1041` through `BR_REWRITE1`, fetched a freed `func_entry` result from the stale table, and then tripped an assertion in `expr::get_sort()` during quantifier model checking. ## Fix After compression removes entries, rebuild `m_entry_table` from the surviving `m_entries`, or clear it when the surviving interpretation is small. ## Regression coverage Added a unit regression in `src/test/model_evaluator.cpp` that: - creates a `func_interp` large enough to allocate `m_entry_table`, - compresses away almost all entries, - checks that removed keys no longer resolve, and - checks that the surviving key still resolves to the correct result. ## Validation - `../build/z3 ebso-115.smt2` previously hit an assertion in `rewriter_def.h` / `ast.cpp`; after the fix it no longer asserts. - `./test-z3 model_evaluator` passes with the new regression. ## Reproducer I did not produce a smaller SMT2 benchmark in this change. The original reproducer I used was `ebso-115.smt2`, and the new unit regression directly exercises the stale-entry-table path in-process. Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||