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

z3str3: don't crash when finding initial bounds for a regex that has no solutions (#4276)

Browse source
This commit is contained in:
Murphy Berzish 2020-05-11 19:41:55 -05:00 committed by GitHub
parent e254e890a1
commit bd0180925b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str_regex.cpp
View file

@ -1154,8 +1154,9 @@ namespace smt {
expr_ref rhs2(m_autil.mk_ge(strlen, m_autil.mk_numeral(nonzero_lower_bound, true)), m); expr_ref rhs2(m_autil.mk_ge(strlen, m_autil.mk_numeral(nonzero_lower_bound, true)), m);
rhs.push_back(rhs2); rhs.push_back(rhs2);
} else { } else {
// shouldn't happen // probably no solutions at all; just assume that 0 is a (safe) lower bound
UNREACHABLE(); regex_last_lower_bound.insert(str, rational::zero());
rhs.reset();
} }
} }
// TODO upper bound check // TODO upper bound check