diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp
index e30e857b2..bc64e7218 100644
--- a/src/ast/rewriter/str_rewriter.cpp
+++ b/src/ast/rewriter/str_rewriter.cpp
@@ -456,10 +456,10 @@ br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result)
 	// fast path:
 	// (RegexIn E (Str2Reg S)) --> (= E S)
 	if (m_strutil.is_re_Str2Reg(re)) {
-		TRACE("t_str_rw", tout << "RegexIn fast path: " << mk_pp(str, m()) << " in " << mk_pp(re, m()) << std::endl;);
 		expr * regexStr = to_app(re)->get_arg(0);
 		ENSURE(m_strutil.is_string(regexStr));
 		result = m().mk_eq(str, regexStr);
+		TRACE("t_str_rw", tout << "RegexIn fast path: " << mk_pp(str, m()) << " in " << mk_pp(re, m()) << " ==> " << mk_pp(result, m()) << std::endl;);
 		return BR_REWRITE_FULL;
 	}
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 37be73333..543adcc03 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1708,6 +1708,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) {
     	expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
     	SASSERT(finalAxiom);
     	assert_axiom(finalAxiom);
+    	TRACE("t_str", tout << "set up Str2Reg: (RegexIn " << mk_pp(str, m) << " " << mk_pp(regex, m) << ")" << std::endl;);
     } else if (is_RegexConcat(regex)) {
     	expr_ref var1(mk_regex_rep_var(), m);
     	expr_ref var2(mk_regex_rep_var(), m);