From 4fc64ab578ab75f96381ee60a15f879af3cde9ea Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 11 Oct 2019 11:56:52 -0400
Subject: [PATCH] z3str3: check for and re-internalize str.in.re terms

---
 src/smt/theory_str.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a30dbd551..824f6c595 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9926,6 +9926,12 @@ namespace smt {
             expr * str = nullptr;
             expr * re = nullptr;
             u.str.is_in_re(str_in_re, str, re);
+            if (!ctx.b_internalized(str_in_re)) {
+                TRACE("str", tout << "regex term " << mk_pp(str_in_re, m) << " not internalized; fixing and continuing" << std::endl;);
+                ctx.internalize(str_in_re, false);
+                finalCheckProgressIndicator = true;
+                continue;
+            }
             lbool current_assignment = ctx.get_assignment(str_in_re);
             TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;);
             if (current_assignment == l_undef) {