mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add parameter validation in two remaining local cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-14 11:29:05 -07:00
parent 0e4e72b1bc
commit 10c5ed6344
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_solver.cpp
View file

@ -130,6 +130,9 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_solver_set_params(c, s, p); LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE(); 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) { if (to_solver(s)->m_solver) {
bool old_model = to_solver(s)->m_params.get_bool("model", true); bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).get_bool("model", true); bool new_model = to_param_ref(p).get_bool("model", true);

3
src/api/api_tactic.cpp
View file

@ -450,6 +450,9 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_tactic_apply_ex(c, t, g, p); LOG_Z3_tactic_apply_ex(c, t, g, p);
RESET_ERROR_CODE(); 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)); Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);