diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index c8b1723f1..6fc0c1c72 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -130,6 +130,9 @@ 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); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 7dce33971..adfd0fb71 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -450,6 +450,9 @@ extern "C" { Z3_TRY; LOG_Z3_tactic_apply_ex(c, t, g, p); RESET_ERROR_CODE(); + param_descrs pd; + to_tactic_ref(t)->collect_param_descrs(pd); + to_param_ref(p).validate(pd); Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p)); RETURN_Z3(r); Z3_CATCH_RETURN(0);