diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 9fca36321..55d4a43a8 100644 --- a/src/api/api_polynomial.cpp +++ b/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()); - 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; + + // Compute all polynomial results BEFORE allocating the result vector. + // This avoids a memory corruption issue where allocating API objects + // can interfere with the converter's internal state. + expr_ref_vector results(mk_c(c)->m()); + { + 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 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))) { - expr2var const & mapping = converter.get_mapping(); - 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 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); - } + for (expr* e : results) { + result->m_ast_vector.push_back(e); } RETURN_Z3(of_ast_vector(result)); Z3_CATCH_RETURN(nullptr); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 9aeb79133..b058c58b7 100644 --- a/src/opt/opt_solver.cpp +++ b/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; diff --git a/src/test/api_polynomial.cpp b/src/test/api_polynomial.cpp index 5a01ea0fa..d30469127 100644 --- a/src/test/api_polynomial.cpp +++ b/src/test/api_polynomial.cpp @@ -19,31 +19,63 @@ Notes: #include "api/z3.h" #include "util/trace.h" #include "util/debug.h" +#include + +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 - try { - Z3_ast_vector result = Z3_polynomial_subresultants(ctx, one, two, x); - // If we get here, function executed without major crash - if (result) { - Z3_ast_vector_dec_ref(ctx, result); - } - ENSURE(true); // Test succeeded in calling the function - } catch (...) { - // Even if there's an exception, we tested the function - ENSURE(true); + // Create polynomials: p = x + 1, q = x + 2 + Z3_ast add_args1[2] = {x, one}; + Z3_ast p = Z3_mk_add(ctx, 2, add_args1); + Z3_ast add_args2[2] = {x, two}; + Z3_ast q = Z3_mk_add(ctx, 2, add_args2); + + // Choose which variable to use for subresultant + Z3_ast var; + int choice = var_choice(gen); + switch (choice) { + 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); -} \ No newline at end of file +} + +void tst_api_polynomial() { + // Run multiple tests with fresh contexts + for (int i = 0; i < 20; i++) { + run_single_test(i); + } +}