diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index fb66bb9a1..f4d010632 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2132,10 +2132,14 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
 }
 
 expr_ref seq_rewriter::is_nullable_rec(expr* r) {
+    std::cout << "n";
     expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr, nullptr), m());
     if (!result) {
+        std::cout << "(m) ";
         result = is_nullable(r);
         m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);        
+    } else {
+        std::cout << "(h) ";
     }
     return result;
 }
@@ -2462,10 +2466,13 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
     pair of pointers.
 */
 expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) {
+    std::cout << "c";
     expr_ref result(m_op_cache.find(k, a, b, cond), m());
     if (result) {
+        std::cout << "(h) ";
         return result;
     }
+    std::cout << "(m) ";
     SASSERT((k == OP_ITE) == (cond != nullptr));
     expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr,
          *bcond = nullptr, *b1 = nullptr, *b2 = nullptr;
@@ -2542,6 +2549,7 @@ expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) {
     representation in unfolding string in regex constraints.
 */
 expr_ref seq_rewriter::lift_ites(expr* r, bool lift_over_union, bool lift_over_inter) {
+    std::cout << "l ";
     decl_kind k = to_app(r)->get_decl_kind();
     family_id fid = get_fid();
     expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr;
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index ee1484125..675893381 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -101,6 +101,8 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var());
         VERIFY(str().is_in_re(e, s, r));
 
+        std::cout << "PI ";
+
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         // convert negative negative membership literals to positive
@@ -144,6 +146,7 @@ namespace smt {
     }
 
     void seq_regex::propagate_accept(literal lit) {
+        std::cout << "PA ";
         if (!propagate(lit))
             m_to_propagate.push_back(lit);
     }
@@ -197,6 +200,9 @@ namespace smt {
 
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
+        std::cout << "P ";
+        // << mk_pp(e, m) << std::endl;
+
         if (block_unfolding(lit, idx))
             return true;
 
@@ -314,6 +320,7 @@ namespace smt {
         with optimizations for if-then-else expressions involving the head.
     */
     expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
+        std::cout << "D ";
         expr_ref result = expr_ref(re().mk_derivative(hd, r), m);
         rewrite(result);
         // don't lift over unions
@@ -354,6 +361,7 @@ namespace smt {
      *
      */
     void seq_regex::propagate_is_non_empty(literal lit) {
+        std::cout << "PN ";
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_non_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);
@@ -394,6 +402,7 @@ namespace smt {
       is_empty(r, u) is true if r is a member of u
      */
     void seq_regex::propagate_is_empty(literal lit) {
+        std::cout << "PE ";
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);