From bd0180925b6e78c231c2f89027d27b269341a6ad Mon Sep 17 00:00:00 2001
From: Murphy Berzish <mtrberzi@users.noreply.github.com>
Date: Mon, 11 May 2020 19:41:55 -0500
Subject: [PATCH] z3str3: don't crash when finding initial bounds for a regex
 that has no solutions (#4276)

---
 src/smt/theory_str_regex.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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