mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

add special case handling for string constant backpropagation in theory_str

Browse source 
avoid a crash when asserting that a constant string is equal to itself
by not generating this assert in the first place
This commit is contained in:
Murphy Berzish 2017-10-18 16:08:39 -04:00
parent 7f590b5419
commit abdb41c5df
1 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_str.cpp
View file

@ -8888,15 +8888,34 @@ namespace smt {
if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) { if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) {
TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl
<< "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;); << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;);
TRACE("str_enode_bug", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl
<< "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;);
zstring lhsString, rhsString; zstring lhsString, rhsString;
u.str.is_string(concat_lhs_str, lhsString); u.str.is_string(concat_lhs_str, lhsString);
u.str.is_string(concat_rhs_str, rhsString); u.str.is_string(concat_rhs_str, rhsString);
zstring concatString = lhsString + rhsString; zstring concatString = lhsString + rhsString;
expr_ref lhs1(ctx.mk_eq_atom(concat_lhs, concat_lhs_str), m);
expr_ref lhs2(ctx.mk_eq_atom(concat_rhs, concat_rhs_str), m); // special handling: don't assert that string constants are equal to themselves
expr_ref lhs(m.mk_and(lhs1, lhs2), m); expr_ref_vector lhs_terms(m);
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m); if (!u.str.is_string(concat_lhs)) {
assert_implication(lhs, rhs); lhs_terms.push_back(ctx.mk_eq_atom(concat_lhs, concat_lhs_str));
}
if (!u.str.is_string(concat_rhs)) {
lhs_terms.push_back(ctx.mk_eq_atom(concat_rhs, concat_rhs_str));
}
if (lhs_terms.empty()) {
// no assumptions on LHS
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
assert_axiom(rhs);
} else {
expr_ref lhs(mk_and(lhs_terms), m);
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
TRACE("str_enode_bug", tout << "axiom LHS: " << mk_pp(lhs, m) << std::endl;);
TRACE("str_enode_bug", tout << "axiom RHS: " << mk_pp(rhs, m) << std::endl;);
assert_implication(lhs, rhs);
}
backpropagation_occurred = true; backpropagation_occurred = true;
} }
} }