From 35654e7511e5c9bcb024a8ea0ee95ecc62aaecbc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 8 May 2026 17:55:39 +0000 Subject: [PATCH] Refine api_bug sat.smt regression test setup clarity Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/adbdc74f-5aab-4b0e-86a1-4ae2bdb4636e Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/api_bug.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/test/api_bug.cpp b/src/test/api_bug.cpp index 2030a014d..34e43e50e 100644 --- a/src/test/api_bug.cpp +++ b/src/test/api_bug.cpp @@ -16,7 +16,9 @@ static void test_sat_smt_bv_model_reconstruction() { ~sat_smt_guard() { Z3_global_param_set("sat.smt", "false"); } } guard; - Z3_context ctx = Z3_mk_context(nullptr); + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); Z3_solver s = Z3_mk_solver(ctx); Z3_solver_inc_ref(ctx, s); @@ -32,7 +34,8 @@ static void test_sat_smt_bv_model_reconstruction() { Z3_model mdl = Z3_solver_get_model(ctx, s); Z3_model_inc_ref(ctx, mdl); Z3_ast val = nullptr; - ENSURE(Z3_model_eval(ctx, mdl, fml, true, &val)); + constexpr bool model_completion = true; + ENSURE(Z3_model_eval(ctx, mdl, fml, model_completion, &val)); ENSURE(Z3_get_ast_kind(ctx, val) == Z3_APP_AST); Z3_app val_app = Z3_to_app(ctx, val); Z3_func_decl val_decl = Z3_get_app_decl(ctx, val_app);