From 3ee8f27588bcb88220f0ff515526ee0003716c43 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 18 Oct 2015 20:20:09 -0400
Subject: [PATCH] possibly fix internalization bug mentioned in #2 (this leads
 to a not-implemented-yet in final_check_eh() due to missing code surrounding
 free variable production)

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 47165997d..15253bcfd 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1837,6 +1837,8 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
  */
 expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
 	context & ctx = get_context();
+	// I hope this works
+	ctx.internalize(n, false);
 	enode * nNode = ctx.get_enode(n);
 	enode * eqcNode = nNode;
 	do {