From 4d5c1dcfb696a687c0934259b810305669cb4971 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 6 Mar 2017 17:04:07 -0500
Subject: [PATCH] fix model gen for regex terms in theory_str

---
 src/smt/theory_str.h | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 5a67f72f1..54fdc6538 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -63,9 +63,14 @@ namespace smt {
                     m_strings.insert(sym);
                     return u.str.mk_string(sym);
                 }
-            } else {
-                UNREACHABLE(); return NULL;
             }
+            sort* seq = 0;
+            if (u.is_re(s, seq)) {
+                expr* v0 = get_fresh_value(seq);
+                return u.re.mk_to_re(v0);
+            }
+            TRACE("t_str", tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
+            UNREACHABLE(); return NULL;
         }
         virtual void register_value(expr * n) { /* Ignore */ }
     };