diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ee3d3aa71..9b4091724 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -5607,7 +5607,7 @@ expr* seq_rewriter::concat_non_empty(expr_ref_vector& es) {
     sort* s = es[0]->get_sort();
     unsigned j = 0;
     for (expr* e : es) {
-        if (str().is_unit(e) || str().is_string(e))
+        if (str().is_unit(e) || str().is_string(e) || m().is_ite(e))
             es[j++] = e;
     }
     es.shrink(j);
@@ -5623,23 +5623,16 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pa
     zstring s;
     expr* emp = nullptr;
     for (unsigned i = 0; i < sz; ++i) {
-        if (str().is_unit(es[i])) {
-            if (all) return false;
-        }
-        else if (str().is_empty(es[i])) {
+        auto [bounded, len] = min_length(es[i]);
+        if (len > 0) {
+            if (all)
+                return false;
             continue;
         }
-        else if (str().is_string(es[i], s)) {
-            if (s.length() == 0)
-                continue;
-            if (all) {
-                return false;
-            }
-        }
-        else {
-            emp = emp?emp:str().mk_empty(es[i]->get_sort());
-            eqs.push_back(emp, es[i]);
-        }
+        if (bounded && len == 0)
+            continue;
+        emp = emp?emp:str().mk_empty(es[i]->get_sort());
+        eqs.push_back(emp, es[i]);        
     }
     return true;
 }
@@ -5669,6 +5662,9 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
     zstring s;
     unsigned len = 0;
     bool bounded = true;
+
+    if (sz == 0)
+        return { bounded, len };
     expr* c, *th, *el;
     auto visit = [&](expr* e) {
         if (cache.contains(e))
@@ -5703,13 +5699,13 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
             return visited;
         }
         else if (m().is_ite(e, c, th, el)) {
-            unsigned sz = sub.size();
+            unsigned subsz = sub.size();
             std::pair<bool, unsigned> r1, r2;
             if (!cache.find(th, r1))
                 sub.push_back(th);
             if (!cache.find(el, r2))
                 sub.push_back(el);
-            if (sz != sub.size())
+            if (subsz != sub.size())
                 return false;
             
             cache.insert(e, { r1.first && r2.first && r1.second == r2.second, std::min(r1.second, r2.second)});
@@ -5884,6 +5880,16 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
     return false;
 }
 
+bool seq_rewriter::has_var(expr_ref_vector const& es) {
+    for (expr* e : es) {
+        auto [bounded, len] = min_length(e);
+        if (len == 0)
+            return true;
+    }
+    return false;
+}
+
+
 bool seq_rewriter::reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs,
                                     expr_ref_pair_vector& eqs) {
 
@@ -5896,14 +5902,14 @@ bool seq_rewriter::reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs,
         return false;
     if (bounded2 && len2 < len1) 
         return false;
-    if (bounded1 && len1 == len2 && len1 > 0) {
+    if (bounded1 && len1 == len2 && len1 > 0 && has_var(rs)) {
         if (!set_empty(rs.size(), rs.data(), false, eqs))
             return false;
         eqs.push_back(concat_non_empty(ls), concat_non_empty(rs));
         ls.reset(); 
         rs.reset();
     }
-    else if (bounded2 && len1 == len2 && len1 > 0) {
+    else if (bounded2 && len1 == len2 && len1 > 0 && has_var(ls))  {
         if (!set_empty(ls.size(), ls.data(), false, eqs))
             return false;
         eqs.push_back(concat_non_empty(ls), concat_non_empty(rs));
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index eecf032b6..4c7c3883a 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -322,6 +322,7 @@ class seq_rewriter {
     bool reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
+    bool has_var(expr_ref_vector const& es);
     bool reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
     bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);    
     std::pair<bool, unsigned> min_length(expr_ref_vector const& es);