From 1a15b3937deb367adac5c64dae48e9e1298a6b5d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 2 Dec 2015 22:09:30 -0500
Subject: [PATCH] in_same_eqc() now checks to ensure both terms are
 internalized before doing anything else

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 9b9cc8fd9..62100cfcd 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1999,6 +1999,20 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
 bool theory_str::in_same_eqc(expr * n1, expr * n2) {
     if (n1 == n2) return true;
     context & ctx = get_context();
+    ast_manager & m = get_manager();
+
+    // similar to get_eqc_value(), make absolutely sure
+    // that we've set this up properly for the context
+
+    if (!ctx.e_internalized(n1)) {
+        TRACE("t_str_detail", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;);
+        ctx.internalize(n1, false);
+    }
+    if (!ctx.e_internalized(n2)) {
+        TRACE("t_str_detail", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;);
+        ctx.internalize(n2, false);
+    }
+
     enode * n1Node = ctx.get_enode(n1);
     enode * n2Node = ctx.get_enode(n2);