mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
z3str3: fix up regex heuristics (#4342)
fixes #4308, partially fixes #4309
This commit is contained in:
parent
bfb38451d1
commit
3147be66fe
|
@ -910,7 +910,7 @@ namespace smt {
|
|||
return check_regex_length_linearity_helper(sub1, already_star);
|
||||
} else {
|
||||
TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
|
||||
UNREACHABLE(); return false;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1144,8 +1144,9 @@ namespace smt {
|
|||
expr_ref rhs2(m_autil.mk_ge(strlen, m_autil.mk_numeral(nonzero_lower_bound, true)), m);
|
||||
rhs.push_back(m.mk_or(rhs1, rhs2));
|
||||
} else {
|
||||
// shouldn't happen
|
||||
UNREACHABLE();
|
||||
// length of solution can ONLY be 0
|
||||
expr_ref rhs1(ctx.mk_eq_atom(strlen, m_autil.mk_numeral(rational::zero(), true)), m);
|
||||
rhs.push_back(rhs1);
|
||||
}
|
||||
} else {
|
||||
// no solution at 0
|
||||
|
|
Loading…
Reference in a new issue