From f1d7ffcdced6635717911f18c57d46b2af0c69bf Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 20 Sep 2016 00:14:38 -0400
Subject: [PATCH] fix regression regex-020

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8cd7c227c..44a4b0d7c 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -7641,9 +7641,9 @@ final_check_status theory_str::final_check_eh() {
         get_eqc_value(*it, has_eqc_value);
         if (!has_eqc_value) {
             // if this is an internal variable, it can be ignored...I think
-            if (internal_variable_set.find(*it) != internal_variable_set.end()) {
+            if (internal_variable_set.find(*it) != internal_variable_set.end() || regex_variable_set.find(*it) != regex_variable_set.end()) {
                 TRACE("t_str_detail", tout << "WARNING: free internal variable " << mk_ismt2_pp(*it, m) << std::endl;);
-                unused_internal_variables.insert(*it);
+                //unused_internal_variables.insert(*it);
             } else {
                 needToAssignFreeVars = true;
                 free_variables.insert(*it);