preserve the initial state of the solver with push/pop for multiple objectives (#8264)

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

src/api/api_polynomial.cpp

@@ -33,34 +33,48 @@ extern "C" {
         LOG_Z3_polynomial_subresultants(c, p, q, x);
         RESET_ERROR_CODE();
         polynomial::manager & pm = mk_c(c)->pm();
-        polynomial_ref _p(pm), _q(pm);
+
-        polynomial::scoped_numeral d(pm.m());
+        // Compute all polynomial results BEFORE allocating the result vector.
-        default_expr2polynomial converter(mk_c(c)->m(), pm);
+        // This avoids a memory corruption issue where allocating API objects
-        if (!converter.to_polynomial(to_expr(p), _p, d) ||
+        // can interfere with the converter's internal state.
-            !converter.to_polynomial(to_expr(q), _q, d)) {
+        expr_ref_vector results(mk_c(c)->m());
-            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+        {
-            return nullptr;
+            polynomial_ref _p(pm), _q(pm);
+            polynomial::scoped_numeral d(pm.m());
+            default_expr2polynomial converter(mk_c(c)->m(), pm);
+            if (!converter.to_polynomial(to_expr(p), _p, d) ||
+                !converter.to_polynomial(to_expr(q), _q, d)) {
+                SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+                return nullptr;
+            }
+
+            if (converter.is_var(to_expr(x))) {
+                expr2var const & mapping = converter.get_mapping();
+                unsigned v_x = mapping.to_var(to_expr(x));
+                if (v_x != UINT_MAX) {
+                    polynomial_ref_vector rs(pm);
+                    polynomial_ref r(pm);
+                    expr_ref _r(mk_c(c)->m());
+
+                    {
+                        cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
+                        api::context::set_interruptable si(*(mk_c(c)), eh);
+                        scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
+                        pm.psc_chain(_p, _q, v_x, rs);
+                    }
+                    for (unsigned i = 0; i < rs.size(); ++i) {
+                        r = rs.get(i);
+                        converter.to_expr(r, true, _r);
+                        results.push_back(_r);
+                    }
+                }
+            }
         }
+        // Converter is now out of scope - safe to allocate result vector
         Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(result);
-        if (converter.is_var(to_expr(x))) {
+        for (expr* e : results) {
-            expr2var const & mapping = converter.get_mapping();
+            result->m_ast_vector.push_back(e);
-            unsigned v_x = mapping.to_var(to_expr(x));
-            polynomial_ref_vector rs(pm);
-            polynomial_ref r(pm);
-            expr_ref _r(mk_c(c)->m());
-
-            {
-                cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
-                api::context::set_interruptable si(*(mk_c(c)), eh);
-                scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
-                pm.psc_chain(_p, _q, v_x, rs);
-            }
-            for (unsigned i = 0; i < rs.size(); ++i) {
-                r = rs.get(i);
-                converter.to_expr(r, true, _r);
-                result->m_ast_vector.push_back(_r);
-            }
         }
         RETURN_Z3(of_ast_vector(result));
         Z3_CATCH_RETURN(nullptr);

src/opt/opt_solver.cpp

@@ -202,8 +202,29 @@ namespace opt {
     bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
         expr_ref blocker(m);
         for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
-            if (!maximize_objective(i, blocker))
+            // Push context to isolate each objective's optimization.
+            // This prevents bounds created during one objective's optimization
+            // from affecting subsequent objectives (fixes issue #7677).
+            m_context.push();
+
+            if (!maximize_objective(i, blocker)) {
+                m_context.pop(1);
                 return false;
+            }
+
+            // Save results before popping
+            inf_eps val = m_objective_values[i];
+            model_ref mdl;
+            if (m_models[i])
+                mdl = m_models[i];
+
+            m_context.pop(1);
+
+            // Restore the computed values after pop
+            m_objective_values[i] = val;
+            if (mdl)
+                m_models.set(i, mdl.get());
+
             blockers.push_back(blocker);
         }
         return true;

src/test/api_polynomial.cpp

@@ -19,31 +19,63 @@ Notes:
 #include "api/z3.h"
 #include "util/trace.h"
 #include "util/debug.h"
+#include <random>
+
+static void run_single_test(int seed) {
+    std::mt19937 gen(seed);
+    std::uniform_int_distribution<> var_choice(0, 2);
 
-void tst_api_polynomial() {
     Z3_config cfg = Z3_mk_config();
     Z3_context ctx = Z3_mk_context(cfg);
     Z3_del_config(cfg);
 
-    // Create real sort and simple variables
     Z3_sort real_sort = Z3_mk_real_sort(ctx);
+
+    // Create variables
     Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
+    Z3_symbol y_sym = Z3_mk_string_symbol(ctx, "y");
+    Z3_symbol z_sym = Z3_mk_string_symbol(ctx, "z");
     Z3_ast x = Z3_mk_const(ctx, x_sym, real_sort);
+    Z3_ast y = Z3_mk_const(ctx, y_sym, real_sort);
+    Z3_ast z = Z3_mk_const(ctx, z_sym, real_sort);
+
+    // Constants
     Z3_ast one = Z3_mk_real(ctx, 1, 1);
     Z3_ast two = Z3_mk_real(ctx, 2, 1);
 
-    // Test Z3_polynomial_subresultants - just try to call it
+    // Create polynomials: p = x + 1, q = x + 2
-    try {
+    Z3_ast add_args1[2] = {x, one};
-        Z3_ast_vector result = Z3_polynomial_subresultants(ctx, one, two, x);
+    Z3_ast p = Z3_mk_add(ctx, 2, add_args1);
-        // If we get here, function executed without major crash
+    Z3_ast add_args2[2] = {x, two};
-        if (result) {
+    Z3_ast q = Z3_mk_add(ctx, 2, add_args2);
-            Z3_ast_vector_dec_ref(ctx, result);
+
-        }
+    // Choose which variable to use for subresultant
-        ENSURE(true); // Test succeeded in calling the function
+    Z3_ast var;
-    } catch (...) {
+    int choice = var_choice(gen);
-        // Even if there's an exception, we tested the function
+    switch (choice) {
-        ENSURE(true);
+        case 0: var = x; break;  // x is in the polynomials
+        case 1: var = y; break;  // y is NOT in the polynomials
+        default: var = z; break; // z is NOT in the polynomials
     }
 
+    Z3_ast_vector result = Z3_polynomial_subresultants(ctx, p, q, var);
+    ENSURE(result != nullptr);
+    Z3_ast_vector_inc_ref(ctx, result);  // Take ownership
+    unsigned size = Z3_ast_vector_size(ctx, result);
+    // If var is x (in polynomials), expect 1 result; otherwise 0
+    if (choice == 0) {
+        ENSURE(size == 1);
+    } else {
+        ENSURE(size == 0);
+    }
+    Z3_ast_vector_dec_ref(ctx, result);  // Release ownership
+
     Z3_del_context(ctx);
 }
+
+void tst_api_polynomial() {
+    // Run multiple tests with fresh contexts
+    for (int i = 0; i < 20; i++) {
+        run_single_test(i);
+    }
+}