diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index 394edfb334..69f5dea165 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -458,7 +458,7 @@ struct split_set::iterator::imp {
         // where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining
         // j in [l,h] with j > i, into a single loop [<eps,eps> when l == 0]
         unsigned l, h;
-        if (re.is_loop(r, a, l, h)) {
+        if (false && re.is_loop(r, a, l, h)) {
             if (l == 0) {
                 auto eps = mk_eps();
                 push_split(eps, eps);
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 289ca5e0f8..6f3c8609c3 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -444,8 +444,6 @@ namespace smt {
         // Final check also unfolds this axiomatization
         // (we have to add a final check to seq_regex for this).
 
-
-
         unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold;
         expr_ref_vector prefix(m);
         expr *hd, *tl, *v;
@@ -477,8 +475,7 @@ namespace smt {
             }
             if (!result.failed()) {
                 const expr_ref cases_expr(m.mk_or(cases), m);
-                ctx.internalize(cases_expr, false);
-                th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr));
+                th.propagate_lit(nullptr, 1, &lit, th.mk_literal(cases_expr));
                 return true;
             }
         }