diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index f84546282b..9892ffd35c 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -235,6 +235,19 @@ namespace seq {
             return mk_inter(d1, d2);
         }
 
+        // handle unary unsimplified cases of operators
+        if (re().is_union(r, r1)) 
+            return derive_rec(r1);
+
+        if (re().is_intersection(r, r1))
+            return derive_rec(r1);
+
+        if (re().is_concat(r, r1))
+            return derive_rec(r1);
+
+        if (re().is_xor(r, r1))
+            return derive_rec(r1);
+
         // δ(~r1) = ~δ(r1)
         if (re().is_complement(r, r1)) {
             expr_ref d1 = derive_rec(r1);
diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp
index 1ec4335f95..ecd1903997 100644
--- a/src/ast/rewriter/seq_monadic.cpp
+++ b/src/ast/rewriter/seq_monadic.cpp
@@ -29,12 +29,17 @@ TODOs:
   - coallesce the membership constraints into a single regex membership constraint of the intersection of regexes.
 - take into account shape of terms to prune the search space (e.g., if the term is xax, then retain the effect of 
   intersecting with .*a.*).
-- use expr_ref in component and replace svector<component> by vector<component>, save on m_pin.
+- connect to semi-linear pruning, such as xx in (ab)*a is unsat due to parity 
 - support units of non-values (element variables).
   Model construction would assign values to the elements.
 - make unsat core tracking less naive by tracking dependencies at a finer grain.
-- add statistics and use it from src/smt/seq_regex.cpp when extracting statistics from theory_seq.
 - add selective tracing TRACE(seq, ..).
+- revisit DFS to select next membership constraint to explore base on the current state.
+  In the current state include current set of variable intersection membership constraints.
+  The next membership constraint to explore is preferrably for a variable that was just
+  explored and we can check the variable intersection membership constraints if the new
+  expansion is feasible. Constant characters are consumed at the same time to also prune
+  the choice.
 
 
 
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 8566173f2b..12995a6f1d 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -593,6 +593,10 @@ public:
         MATCH_BINARY(is_diff);
         MATCH_BINARY(is_xor);
         MATCH_BINARY(is_range);
+        MATCH_UNARY(is_concat);
+        MATCH_UNARY(is_union);
+        MATCH_UNARY(is_intersection);
+        MATCH_UNARY(is_xor);
         MATCH_UNARY(is_complement);
         MATCH_UNARY(is_star);
         MATCH_UNARY(is_plus);