* 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>
