From bed40c45b80d83ed7ad82ef14ec92f3b8352854b Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 14 Sep 2016 21:48:27 -0400
Subject: [PATCH] cleanup

---
 src/smt/theory_str.cpp | 10 ++++++----
 src/smt/theory_str.h   |  2 ++
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index dbf5d2f38..1dcfb0b29 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2161,6 +2161,7 @@ expr * theory_str::simplify_concat(expr * node) {
         if (in_same_eqc(node, resultAst)) {
             TRACE("t_str_detail", tout << "SKIP: both concats are already in the same equivalence class" << std::endl;);
         } else {
+            // TODO refactor
             expr ** items = alloc_svect(expr*, resolvedMap.size());
             int pos = 0;
             std::map<expr*, expr*>::iterator itor = resolvedMap.begin();
@@ -2459,8 +2460,8 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) {
         }
     }
 
-    expr * new_nn1 = simplify_concat(nn1);
-    expr * new_nn2 = simplify_concat(nn2);
+    expr_ref new_nn1(simplify_concat(nn1), m);
+    expr_ref new_nn2(simplify_concat(nn2), m);
     app * a_new_nn1 = to_app(new_nn1);
     app * a_new_nn2 = to_app(new_nn2);
 
@@ -5466,8 +5467,6 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
 
     items.push_back(ctx.mk_eq_atom(n1, n2));
 
-    expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr);
-
     bool conflict = false;
 
     if (concat1LenFixed && concat2LenFixed) {
@@ -5486,6 +5485,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
 
     if (conflict) {
         TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;);
+        expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr);
         assert_axiom(toAssert);
         return false;
     }
@@ -6619,10 +6619,12 @@ void theory_str::dump_assignments() {
 	tout << "dumping all assignments:" << std::endl;
 	expr_ref_vector assignments(m);
 	ctx.get_assignments(assignments);
+	/*
 	for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
 		expr * ex = *i;
 		tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? "" : " (NOT REL)") << std::endl;
 	}
+	*/
 	);
 }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 745d22ac2..7af6ab1ca 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -29,6 +29,8 @@ Revision History:
 #include"str_rewriter.h"
 #include"union_find.h"
 
+// TODO refactor: anything that returns an expr* instead returns an expr_ref
+
 namespace smt {
 
     class str_value_factory : public value_factory {