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

fix #5154

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-07 11:28:51 -07:00
parent 46831e7ebb
commit a99e75f58f
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/params/smt_params.cpp
View file

@ -50,6 +50,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_core_validate = p.core_validate();
m_logic = _p.get_sym("logic", m_logic);
m_string_solver = p.string_solver();
validate_string_solver(m_string_solver);
if (_p.get_bool("arith.greatest_error_pivot", false))
m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_GREATEST_ERROR;
else if (_p.get_bool("arith.least_error_pivot", false))
@ -173,3 +174,9 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_dump_goal_as_smt);
DISPLAY_PARAM(m_auto_config);
}
void smt_params::validate_string_solver(symbol const& s) const {
if (s == "z3str3" || s == "seq" || s == "empty" || s == "auto" || s == "none")
return;
throw default_exception("Invalid string solver value. Legal values are z3str3, seq, empty, auto, none");
}

2
src/smt/params/smt_params.h
View file

@ -320,6 +320,8 @@ struct smt_params : public preprocessor_params,
void updt_params(context_params const & p);
void display(std::ostream & out) const;
void validate_string_solver(symbol const& s) const;
};