diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index f7eba5694..f0d4fd806 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -514,9 +514,17 @@ namespace euf {
         if (n->is_empty() || n->is_char())
             return n;
         if (n->is_concat()) {
-            return mk_concat(subst(n->arg(0), var, replacement),
-                                      subst(n->arg(1), var, replacement));
+            auto s1 = subst(n->arg(0), var, replacement);
+            auto s2 = subst(n->arg(1), var, replacement);
+            if (s1 != n->arg(0) || s2 != n->arg(1))
+                return mk_concat(s1, s2);
+            else
+                return n;
         }
+        // substitution can also work for expressions under unit.
+        // this unifies two kinds of substitutions used in ZIPT (right Clemens ?).
+        if (n->is_unit() && n->arg(0) == var)
+            return mk(m_seq.str.mk_unit(replacement->get_expr()));
         // for non-concat compound nodes (power, star, etc.), no substitution into children
         return n;
     }
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index a19b52117..34551ca38 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2546,6 +2546,14 @@ namespace seq {
                 var = r;
                 def = l;
             }
+            else if (l->is_unit() && l->arg(0)->is_var() && m_seq.str.is_unit(r->get_expr())) {
+                var = l->arg(0);
+                def = r->arg(0);
+            }
+            else if (r->is_unit() && r->arg(0)->is_var() && m_seq.str.is_unit(l->get_expr())) {
+                var = r->arg(0);
+                def = l->arg(0);
+            }
 
 
             if (var) {