From 3147be66fe142a1b5e3d312346fc1fe900b805bd Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 16 May 2020 19:17:32 -0500 Subject: [PATCH] z3str3: fix up regex heuristics (#4342) fixes #4308, partially fixes #4309 --- src/smt/theory_str_regex.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 55ed8e1a0..b26959e49 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -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