diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index 8a9051fa2..1aa41c277 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -518,6 +518,8 @@ namespace sls {
             return true;
         if (seq.is_string(e->get_sort()) && strval0(e) == strval1(e))
             return true;
+        SASSERT(!seq.is_string(e->get_sort()) || strval0(e).length() >= get_eval(e).min_length);
+        SASSERT(!seq.is_string(e->get_sort()) || strval0(e).length() <= get_eval(e).max_length);
         if (e->get_family_id() == m_fid)
             return repair_down_seq(e);
         if (m.is_eq(e))
@@ -1314,7 +1316,7 @@ namespace sls {
                     zstring new_x = sx;
                     while (new_x.length() < r)
                         new_x += zstring(!m_chars.empty() ? m_chars[ctx.rand(m_chars.size())] : zstring("a"));
-                    new_x += se;
+                    new_x = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_x + se);
                     m_str_updates.push_back({ x, new_x, 1 });
                 }
             }
@@ -1512,6 +1514,7 @@ namespace sls {
     bool seq_plugin::repair_down_str_extract(app* e) {
         expr* x, * offset, * len;
         VERIFY(seq.str.is_extract(e, x, offset, len));
+        SASSERT(strval0(e) != strval1(e));
         zstring v = strval0(e);
         zstring r = strval0(x);
         expr_ref offset_e = ctx.get_value(offset);
@@ -1519,34 +1522,36 @@ namespace sls {
         rational offset_val, len_val;
         VERIFY(a.is_numeral(offset_e, offset_val));
         VERIFY(a.is_numeral(len_e, len_val));
-        if (v.empty() && (offset_val.is_neg() || !len_val.is_pos()))
-            return true;
+
+        // std::cout << "repair extract " << mk_bounded_pp(e, m) << " := \"" << v << "\"" << std::endl;
+        // std::cout << "Args: \"" << r << "\" " << offset_val << " " << len_val << std::endl;
+
+        unsigned offset_u = offset_val.is_unsigned() ? offset_val.get_unsigned() : 0;
+        unsigned len_u = len_val.is_unsigned() ? len_val.get_unsigned() : 0;
+        bool has_empty = false;
+
         if (offset_val.is_neg() || offset_val.get_unsigned() >= r.length()) {
-            m_str_updates.push_back({ e, zstring(), 1 });
+            has_empty = true;
             for (unsigned i = 0; i < r.length(); i++)
                 m_int_updates.push_back({ offset, rational(i), 1 });
         }
 
         if (!len_val.is_pos()) {
-            m_str_updates.push_back({ e, zstring(), 1 });
-            for (unsigned i = 1; i < r.length() - offset_val.get_unsigned(); i++)
+            has_empty = true;
+            for (unsigned i = 1; i + offset_u < r.length(); i++)
                 m_int_updates.push_back({ len, rational(i), 1 });
         }
-        if (offset_val.is_unsigned() && len_val.is_unsigned() && v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned()))
-            return true;
 
-        SASSERT(offset_val.is_unsigned());
-        SASSERT(len_val.is_unsigned());
-        unsigned offset_u = offset_val.get_unsigned();
-        unsigned len_u = len_val.get_unsigned();
+        if (has_empty)
+            m_str_updates.push_back({ e, zstring(), 1 });
 
         zstring prefix = r.extract(0, offset_u);
         zstring suffix = r.extract(offset_u + len_u, r.length());
         zstring new_r = prefix + v + suffix;
-        
+
         new_r = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_r);
 
-        if (new_r == r)
+        if (new_r != r)
             m_str_updates.push_back({ x, new_r, 1 });
 
         return apply_update();
@@ -1672,7 +1677,9 @@ namespace sls {
             if (is_str_update) {
                 auto [e, value, score] = m_str_updates[i];
 
+                // std::cout << "Trying str-update: " <<  mk_pp(e, m) << " := \"" << value << "\"" << std::endl;
                 if (update(e, value)) {
+                    // std::cout << "Success" << std::endl;
                     IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := \"" << value << "\"\n");
                     m_str_updates.reset();
                     m_int_updates.reset();
@@ -1688,7 +1695,9 @@ namespace sls {
 
                 IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := " << value << "\n");
 
+                // std::cout << "Trying int-update: " <<  mk_pp(e, m) << " := " << value << std::endl;
                 if (update(e, value)) {
+                    // std::cout << "Success" << std::endl;
                     m_int_updates.reset();
                     m_str_updates.reset();
                     return true;
@@ -1699,12 +1708,13 @@ namespace sls {
             }
         }
 
+        std::cout << "No candidate found" << std::endl;
         return false;
     }
 
     bool seq_plugin::update(expr* e, zstring const& value) {
         SASSERT(value != strval0(e));
-        std::cout << "update " << mk_pp(e, m) << " := \"" << value << "\" [\"" << strval0(e) << "\"]" << std::endl;
+        // std::cout << "str-update " << mk_pp(e, m) << " := \"" << value << "\" [\"" << strval0(e) << "\"]" << std::endl;
         // if (value == strval0(e))
         //     return true;
         if (is_value(e))