From 6e31d9c3f55ef3745d6f5929864cf6e96c79573d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 30 Oct 2017 14:34:27 -0400
Subject: [PATCH] internalize free var before iterating eqc in theory_str

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index fc8122800..f47d6011f 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -10484,6 +10484,9 @@ namespace smt {
             // iterate parents
             if (standAlone) {
                 // I hope this works!
+                if (!ctx.e_internalized(freeVar)) {
+                    ctx.internalize(freeVar, false);
+                }
                 enode * e_freeVar = ctx.get_enode(freeVar);
                 enode_vector::iterator it = e_freeVar->begin_parents();
                 for (; it != e_freeVar->end_parents(); ++it) {