diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 37ea297c2..7271048b1 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1829,7 +1829,6 @@ void ast_manager::delete_node(ast * n) {
         TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";);
         CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
         TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
-        TRACE("t_str_refcount_hack", tout << "delete ast " << n->m_id << std::endl;);
         TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
 
         SASSERT(m_ast_table.contains(n));
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7532bf3f8..29321ecf7 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2403,9 +2403,6 @@ namespace smt {
     */
     unsigned context::pop_scope_core(unsigned num_scopes) {
 
-        TRACE("t_str_refcount_hack", tout << "begin pop_scope_core in smt_context" << std::endl;);
-
-
         if (m_manager.has_trace_stream())
             m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
 
@@ -2453,9 +2450,7 @@ namespace smt {
         ptr_vector<theory>::iterator it  = m_theory_set.begin();
         ptr_vector<theory>::iterator end = m_theory_set.end();
         for (; it != end; ++it) {
-            TRACE("t_str_refcount_hack", tout << "begin theory pop_scope_eh" << std::endl;);
             (*it)->pop_scope_eh(num_scopes);
-            TRACE("t_str_refcount_hack", tout << "end theory pop_scope_eh" << std::endl;);
         }
 
         del_justifications(m_justifications, s.m_justifications_lim);
@@ -2482,9 +2477,6 @@ namespace smt {
         reassert_units(units_to_reassert_lim);
         TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
         CASSERT("context", check_invariant());
-
-        TRACE("t_str_refcount_hack", tout << "end pop_scope_core in smt_context" << std::endl;);
-
         return num_bool_vars;
     }
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 84295940a..b78cbbe59 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1793,7 +1793,6 @@ void theory_str::reset_eh() {
  * Then add an assertion: (y2 == (Concat ce m2)) AND ("str3" == (Concat abc x2)) -> (y2 != "str3")
  */
 bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
-    TRACE("t_str_refcount_hack", tout << "begin new_eq_check in theory_str" << std::endl;);
     context & ctx = get_context();
     ast_manager & m = get_manager();
 
@@ -1819,7 +1818,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
                 expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
                 assert_axiom(to_assert);
                 // this shouldn't use the integer theory at all, so we don't allow the option of quick-return
-                TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
                 return false;
             }
             if (!check_length_consistency(eqc_nn1, eqc_nn2)) {
@@ -1827,7 +1825,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
                 if (opt_NoQuickReturn_IntegerTheory){
                     TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;);
                 } else {
-                    TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
                     return false;
                 }
             }
@@ -1846,7 +1843,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
     }
 
     // okay, all checks here passed
-    TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
     return true;
 }
 
@@ -7276,20 +7272,11 @@ void theory_str::check_variable_scope() {
 }
 
 void theory_str::pop_scope_eh(unsigned num_scopes) {
-    TRACE("t_str_refcount_hack", tout << "begin pop_scope_eh in theory_str" << std::endl;);
-
     sLevel -= num_scopes;
     TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
     context & ctx = get_context();
     ast_manager & m = get_manager();
 
-    // {
-    // expr_ref_vector assignments(m);
-    // ctx.get_assignments(assignments);
-    // TRACE("t_str_refcount_hack", tout << "assignment vector about to go out of scope" << std::endl;);
-    // }
-    // TRACE("t_str_refcount_hack", tout << "assignment vector has gone out of scope" << std::endl;);
-
     TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });
 
     // list of expr* to remove from cut_var_map
@@ -7337,8 +7324,6 @@ void theory_str::pop_scope_eh(unsigned num_scopes) {
     theory::pop_scope_eh(num_scopes);
 
     //check_variable_scope();
-
-    TRACE("t_str_refcount_hack", tout << "end pop_scope_eh in theory_str" << std::endl;);
 }
 
 void theory_str::dump_assignments() {