diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index 6b5045e2b2..40afd7cb1d 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -882,15 +882,7 @@ class seq_expr_inverter : public iexpr_inverter {
             return false;
         case OP_SEQ_IN_RE:
             if (uncnstr(args[0]) && seq.re.is_ground(args[1]) && seq.is_string(args[0]->get_sort())) {
-#if 0
-                //
-                // requires auxiliary functions
-                // some_string_in_re.
-                // A preliminary implementation exists in sls_seq_plugin.cpp
-                // it should be moved to seq_rewriter and made agnostic to m_chars.
-                // maybe use backtracking for better covereage: when some_string_in_re
-                // fails it doesn't necessarily mean that the regex is empty.
-                //
+#if 1
                 zstring s1, s2;
                 expr* re = args[1];
                 expr_ref not_re(seq.re.mk_complement(re), m);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 7598be803a..7651314260 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -6153,6 +6153,7 @@ bool seq_rewriter::some_string_in_re(expr* r, zstring& s) {
     expr_mark visited;
     unsigned_vector str;
     expr_ref_vector pinned(m());
+
     if (!some_string_in_re(pinned, visited, r, str))
         return false;
     s = zstring(str.size(), str.data());
@@ -6198,29 +6199,29 @@ bool seq_rewriter::append_char(expr_ref_vector& pinned, expr_mark& visited, buff
         if (append_char(pinned, visited, exclude, el, str))
             return true;
         exclude.pop_back();
+        return false;
     }
 
     if (is_ground(r)) {
         // ensure selected character is not in exclude
         unsigned ch = 'a';
-        bool at_base = false;
+        bool wrapped = false;
         while (true) {
             bool found = false;
             for (auto [l, h] : exclude) {
                 if (l <= ch && ch <= h) {
                     found = true;
                     ch = h + 1;
-                    break;
                 }
             }
             if (!found)
                 break;
-            if (ch == zstring::unicode_max_char() + 1) {
-                if (at_base) 
-                    return false;
-                ch = 0; 
-                at_base = true;
-            }
+            if (ch != zstring::unicode_max_char() + 1)
+                continue;
+            if (wrapped) 
+                return false;
+            ch = 0; 
+            wrapped = true;            
         }
         str.push_back(ch);
         if (some_string_in_re(pinned, visited, r, str))