diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 8242ca35e..050f0572a 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -20,6 +20,7 @@ Author:
 #include "ast/euf/euf_seq_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "smt/seq/seq_nielsen.h"
 
 namespace euf {
 
@@ -528,6 +529,10 @@ namespace euf {
         expr* elem_expr = elem->get_expr();
         if (!re_expr || !elem_expr)
             return nullptr;
+        // std::cout << "Derivative of " << seq::snode_label_html(re, m) << "\nwith respect to " << seq::snode_label_html(elem, m) << std::endl;
+        // if (allowed_range)
+        //     std::cout << "using " << seq::snode_label_html(allowed_range, m) << std::endl;
+
         
         // unwrap str.unit to get the character expression
         expr* ch = nullptr;
@@ -560,6 +565,7 @@ namespace euf {
             }
             // Fallback: If elem itself is a regex predicate, extract representative
             else if (ele_sort != elem_expr->get_sort()) {
+                // std::cout << "Different sorts: " << ele_sort->get_name() << " vs " << elem_expr->get_sort()->get_name() << std::endl;
                 expr* lo = nullptr, *hi = nullptr;
                 if (m_seq.re.is_full_char(elem_expr))
                     return nullptr;
@@ -573,8 +579,8 @@ namespace euf {
                     else
                         elem_expr = lo;
                 }
-                else
-                    return nullptr;
+                std::cout << "Unexpected node: " << mk_pp(elem_expr, m) << std::endl;
+                UNREACHABLE();
             }
         }
         
@@ -585,9 +591,10 @@ namespace euf {
     }
 
     void sgraph::collect_re_predicates(snode* re, expr_ref_vector& preds) {
-        if (!re || !re->get_expr())
+        if (!re)
             return;
         expr* e = re->get_expr();
+        SASSERT(e);
         expr* lo = nullptr, *hi = nullptr;
         // leaf regex predicates: character ranges and single characters
         if (m_seq.re.is_range(e, lo, hi)) {
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 1e54ac798..81b686caa 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -807,14 +807,36 @@ namespace seq {
 
         if (seq.re.is_to_re(e, a)) {
             zstring s;
-            if (seq.str.is_string(a, s))
-                return "\"" + dot_html_escape(s.encode()) + "\"";
-            unsigned ch_val = 0;
-            if (seq.str.is_unit(a) && seq.is_const_char(to_app(a)->get_arg(0), ch_val)) {
-                return "\"" + dot_html_escape(zstring(ch_val).encode()) + "\"";
-            }
+            bool first = true;
+            svector<expr*> args;
+            args.push_back(a);
+            // flatten concatenations
             std::ostringstream os;
-            os << mk_pp(a, m);
+            while (!args.empty()) {
+                expr* arg = args.back();
+                args.pop_back();
+                if (seq.str.is_concat(arg)) {
+                    args.push_back(to_app(arg)->get_arg(1));
+                    args.push_back(to_app(arg)->get_arg(0));
+                    continue;
+                }
+                if (seq.str.is_string(arg, s)) {
+                    if (!first) os << " ";
+                    os << "\"" + dot_html_escape(s.encode()) + "\"";
+                    first = false;
+                    continue;
+                }
+                unsigned ch_val = 0;
+                if (seq.str.is_unit(arg) && seq.is_const_char(to_app(arg)->get_arg(0), ch_val)) {
+                    if (!first) os << " ";
+                    os << "\"" + dot_html_escape(zstring(ch_val).encode()) + "\"";
+                    first = false;
+                    continue;
+                }
+                if (!first) os << " ";
+                os << mk_pp(arg, m);
+                first = false;
+            }
             return dot_html_escape(os.str());
         }
         if (seq.re.is_concat(e)) {
@@ -833,9 +855,11 @@ namespace seq {
         if (seq.re.is_union(e)) {
             app* ap = to_app(e);
             std::string res;
-            if (ap->get_num_args() == 0) return "&#8709;";
-            for (unsigned i = 0; i < ap->get_num_args(); ++i) {
-                if (i > 0) res += " | ";
+            if (ap->get_num_args() == 0)
+                return "&#8709;";
+            res = regex_expr_html(ap->get_arg(1), m, seq);
+            for (unsigned i = 1; i < ap->get_num_args(); ++i) {
+                res += " | ";
                 res += regex_expr_html(ap->get_arg(i), m, seq);
             }
             return res;
@@ -907,7 +931,7 @@ namespace seq {
     // shows s_power with superscripts, s_unit by its inner expression,
     // and falls back to mk_pp (HTML-escaped) for other token kinds.
 
-    static std::string snode_label_html(euf::snode const* n, ast_manager& m) {
+    std::string snode_label_html(euf::snode const* n, ast_manager& m) {
         if (!n) return "null";
         seq_util seq(m);
 
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 64a5e57c1..88a005a75 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -254,13 +254,16 @@ namespace smt {
     class enode;
 }
 
+
 namespace seq {
 
     // forward declarations
     class nielsen_node;
     class nielsen_edge;
     class nielsen_graph;
-    class seq_parikh;   // Parikh image filter (see seq_parikh.h)
+    class seq_parikh;
+
+    std::string snode_label_html(euf::snode const* n, ast_manager& m);
 
     /**
      * Abstract interface for an incremental solver used by nielsen_graph