mirror of
https://github.com/Z3Prover/z3
synced 2025-08-09 20:50:50 +00:00
bugfix for solver parameters that did not get passed on (codeplex discussion 560796).
Thanks to user xor88 for reporting this issue. Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
5a45711f22
commit
606eeb658e
1 changed files with 1 additions and 0 deletions
|
@ -40,6 +40,7 @@ extern "C" {
|
||||||
params_ref p = s->m_params;
|
params_ref p = s->m_params;
|
||||||
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
|
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
|
||||||
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);
|
||||||
|
s->m_solver->updt_params(p);
|
||||||
}
|
}
|
||||||
|
|
||||||
static void init_solver(Z3_context c, Z3_solver s) {
|
static void init_solver(Z3_context c, Z3_solver s) {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue