diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index e70168498..044ee4523 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4539,6 +4539,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
         result = re().mk_plus(b);
         return BR_DONE;
     }
+    expr *x = nullptr, *y = nullptr;
+    if (re().is_concat(a, x, y) && re().is_full_seq(y) && re().is_full_seq(b)) {
+        result = a;
+        return BR_DONE;
+    }
     expr_ref a_str(m());
     expr_ref b_str(m());
     if (lift_str_from_to_re(a, a_str) && lift_str_from_to_re(b, b_str)) {
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index fdf2e8c0f..ee8eda179 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1502,6 +1502,8 @@ namespace seq {
             IF_VERBOSE(1, display(verbose_stream(), node));
             CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n");
             if (!ext) {
+                std::cout << "No extensions generated for node " << node->id() << ", but not satisfied or conflict?!"
+                          << std::endl;
                 node->to_html(std::cout, m);
                 std::cout << std::endl;
                 display(std::cout, node);