From 5e22bc57c8a484d0891340ab2b095bbc9648cc4a Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 31 Aug 2016 19:19:23 -0400
Subject: [PATCH] theory_str cleanup

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 90b0992d6..9c69f9716 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -3401,7 +3401,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
             std::string part2Str = strValue.substr(i, strValue.size() - i);
             expr_ref cropStr(m_strutil.mk_string(part1Str), mgr);
             expr_ref suffixStr(m_strutil.mk_string(part2Str), mgr);
-            expr_ref y_concat(mk_concat(suffixStr, n), mgr); // TODO concat axioms?
+            expr_ref y_concat(mk_concat(suffixStr, n), mgr);
 
             if (can_two_nodes_eq(x, cropStr) && can_two_nodes_eq(y, y_concat)) {
                 // break down option 3-1
@@ -6435,6 +6435,7 @@ void theory_str::push_scope_eh() {
 void theory_str::pop_scope_eh(unsigned num_scopes) {
     sLevel -= num_scopes;
     TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
+    TRACE("t_str_dump_assign_on_scope_change", dump_assignments(););
 
     std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
     while (varItor != cut_var_map.end()) {