mirror of
https://github.com/Z3Prover/z3
synced 2026-01-27 20:38:42 +00:00
c0583b828d
* preserve the initial state of the solver with push/pop for multiple objectives Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Fix memory corruption in Z3_polynomial_subresultants The API function had a memory corruption bug where allocating the result vector while the default_expr2polynomial converter was still in scope could corrupt the converter's internal expr2var mapping. Fixed by restructuring the code to: 1. Complete all polynomial computation in a scoped block 2. Store results in a temporary expr_ref_vector 3. Let the converter go out of scope 4. Then allocate and populate the result vector Also improved the test to: - Use randomized testing with 20 iterations - Test both cases: variable in polynomials and variable not in polynomials - Use proper reference counting (inc_ref before dec_ref) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| CMakeLists.txt | ||
| maxcore.cpp | ||
| maxcore.h | ||
| maxlex.cpp | ||
| maxlex.h | ||
| maxsmt.cpp | ||
| maxsmt.h | ||
| opt_cmds.cpp | ||
| opt_cmds.h | ||
| opt_context.cpp | ||
| opt_context.h | ||
| opt_cores.cpp | ||
| opt_cores.h | ||
| opt_lns.cpp | ||
| opt_lns.h | ||
| opt_mux.h | ||
| opt_params.pyg | ||
| opt_pareto.cpp | ||
| opt_pareto.h | ||
| opt_parse.cpp | ||
| opt_parse.h | ||
| opt_preprocess.cpp | ||
| opt_preprocess.h | ||
| opt_sls_solver.h | ||
| opt_solver.cpp | ||
| opt_solver.h | ||
| optsmt.cpp | ||
| optsmt.h | ||
| pb_sls.cpp | ||
| pb_sls.h | ||
| sortmax.cpp | ||
| totalizer.cpp | ||
| totalizer.h | ||
| wmax.cpp | ||
| wmax.h | ||