mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Z3str3: safety checks for substr and propagate (#4528)
* z3str3: handle str.substr arguments missing arith values in model construction safely * z3str3: reset propagation vectors on scope pop
This commit is contained in:
parent
7f3bdea0d5
commit
b0633ecc86
|
@ -1000,12 +1000,12 @@ namespace smt {
|
|||
* Length(Concat(x, y)) = Length(x) + Length(y)
|
||||
*/
|
||||
void theory_str::instantiate_concat_axiom(enode * cat) {
|
||||
app * a_cat = cat->get_owner();
|
||||
SASSERT(u.str.is_concat(a_cat));
|
||||
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
app * a_cat = cat->get_owner();
|
||||
TRACE("str", tout << "instantiating concat axiom for " << mk_ismt2_pp(a_cat, m) << std::endl;);
|
||||
if (!u.str.is_concat(a_cat)) {
|
||||
return;
|
||||
}
|
||||
|
||||
// build LHS
|
||||
expr_ref len_xy(m);
|
||||
|
@ -7214,6 +7214,13 @@ namespace smt {
|
|||
TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
|
||||
candidate_model.reset();
|
||||
|
||||
m_basicstr_axiom_todo.reset();
|
||||
m_concat_axiom_todo.reset();
|
||||
m_concat_eval_todo.reset();
|
||||
m_library_aware_axiom_todo.reset();
|
||||
m_delayed_axiom_setup_terms.reset();
|
||||
m_delayed_assertions_todo.reset();
|
||||
|
||||
TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });
|
||||
|
||||
// list of expr* to remove from cut_var_map
|
||||
|
|
|
@ -686,8 +686,14 @@ namespace smt {
|
|||
rational pos, len;
|
||||
bool pos_exists = v.get_value(arg1, pos);
|
||||
bool len_exists = v.get_value(arg2, len);
|
||||
ENSURE(pos_exists);
|
||||
ENSURE(len_exists);
|
||||
if (!pos_exists) {
|
||||
cex = expr_ref(m.mk_or(m_autil.mk_ge(arg1, mk_int(0)), m_autil.mk_le(arg1, mk_int(0))), m);
|
||||
return false;
|
||||
}
|
||||
if (!len_exists) {
|
||||
cex = expr_ref(m.mk_or(m_autil.mk_ge(arg2, mk_int(0)), m_autil.mk_le(arg2, mk_int(0))), m);
|
||||
return false;
|
||||
}
|
||||
TRACE("str_fl", tout << "reduce substring term: base=" << mk_pp(term, m) << " (length="<<base_chars.size()<<"), pos=" << pos.to_string() << ", len=" << len.to_string() << std::endl;);
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
|
|
Loading…
Reference in a new issue