diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 53fe1166d..bf8a52d51 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -391,9 +391,11 @@ extern "C" { bool new_model = params.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); - context_params::collect_solver_param_descrs(r); + param_descrs& r = to_solver(s)->m_param_descrs; + if(r.size () == 0) { + to_solver_ref(s)->collect_param_descrs(r); + context_params::collect_solver_param_descrs(r); + } params.validate(r); to_solver_ref(s)->updt_params(params); } diff --git a/src/api/api_solver.h b/src/api/api_solver.h index 62be1ee60..5214d274c 100644 --- a/src/api/api_solver.h +++ b/src/api/api_solver.h @@ -42,6 +42,7 @@ struct Z3_solver_ref : public api::object { scoped_ptr m_solver_factory; ref m_solver; params_ref m_params; + param_descrs m_param_descrs; symbol m_logic; scoped_ptr m_pp; scoped_ptr m_cmd_context;