From 5c5673bc09435a0477b6e168731d0d67fc3f7f2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Nov 2022 07:55:49 +0700 Subject: [PATCH] make sure parser context within solver object has its parameters updated this is to enable use cases like: ``` from z3 import * s = Solver() OnClause(s, print) s.set("solver.proof.check", False) s.from_file("../satproof.smt2") ``` instead of setting global parameters before the proof replay is initialized. --- src/api/api_solver.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 94d72462f..b93fb42af 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -406,7 +406,11 @@ extern "C" { params.validate(r); to_solver_ref(s)->updt_params(params); } - to_solver(s)->m_params.append(params); + auto& solver = *to_solver(s); + solver.m_params.append(params); + + if (solver.m_cmd_context && solver.m_cmd_context->get_proof_cmds()) + solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params); init_solver_log(c, s); @@ -937,8 +941,10 @@ extern "C" { install_proof_cmds(*solver.m_cmd_context); } - if (!solver.m_cmd_context->get_proof_cmds()) + if (!solver.m_cmd_context->get_proof_cmds()) { init_proof_cmds(*solver.m_cmd_context); + solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params); + } solver.m_cmd_context->get_proof_cmds()->register_on_clause(user_context, _on_clause); Z3_CATCH; }