mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 23:05:26 +00:00
Code Activity

fix #7776

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-13 10:23:51 -07:00
parent c8e866f568
commit 3abb091336
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_solver.cpp
View file

@ -146,6 +146,8 @@ extern "C" {
bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false; bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false;
params_ref p = s->m_params; params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
if (!s->m_solver_factory)
s->m_solver_factory = mk_smt_solver_factory();
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
param_descrs r; param_descrs r;