diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6fc0c1c72..65b2a9047 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,10 @@ extern "C" { 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); 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; + s->m_solver->collect_param_descrs(r); + p.validate(r); s->m_solver->updt_params(p); } @@ -130,14 +134,15 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); - param_descrs r; - to_solver_ref(s)->collect_param_descrs(r); - to_param_ref(p).validate(r); + if (to_solver(s)->m_solver) { bool old_model = to_solver(s)->m_params.get_bool("model", true); bool new_model = to_param_ref(p).get_bool("model", true); if (old_model != new_model) to_solver_ref(s)->set_produce_models(new_model); + param_descrs r; + to_solver_ref(s)->collect_param_descrs(r); + to_param_ref(p).validate(r); to_solver_ref(s)->updt_params(to_param_ref(p)); } to_solver(s)->m_params = to_param_ref(p);