diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index b8835650f..942b96b46 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -98,6 +98,13 @@ Equality solving using stochastic Nelson.
 
 
 namespace sls {
+
+    struct zstring_hash_proc {
+        unsigned operator()(zstring const & s) const {
+            auto str = s.encode();
+            return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17);
+        }
+    };
     
     seq_plugin::seq_plugin(context& c):
         plugin(c),
@@ -666,6 +673,34 @@ namespace sls {
     }
 
 
+    void seq_plugin::add_edit_updates2(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
+        // all consecutive subsequences of val_other
+        map<zstring, bool, zstring_hash_proc, default_eq<zstring>> map;
+        vector<zstring> subseqs;
+        map.insert(zstring(""), true);
+        subseqs.push_back(zstring(""));
+        for (unsigned i = 0; i < val_other.length(); ++i) {
+            for (unsigned j = val_other.length(); j > 0; ++j) {
+                zstring sub = val_other.extract(i, j);
+                if (map.contains(sub))
+                    break;
+                map.insert(sub, true);
+                subseqs.push_back(sub);
+            }
+        }
+
+        for (auto x : w) {
+            if (is_value(x))
+                continue;
+            zstring const& a = strval0(x);
+            for (auto& seq : subseqs) {
+                if (seq == a)
+                    continue;
+                m_str_updates.push_back({ x, seq, 1 });
+            }
+        }
+    }
+
     void seq_plugin::add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
         for (auto x : w) {
             if (is_value(x))
@@ -1487,7 +1522,8 @@ namespace sls {
         for (auto ch : value0) 
             chars.insert(ch);
 
-        add_edit_updates(es, value, value0, chars);
+        // add_edit_updates(es, value, value0, chars);
+        add_edit_updates2(es, value, value0, chars);
 
         unsigned diff = edit_distance(value, value0);
         for (auto& [x, s, score] : m_str_updates) {
diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h
index bd34b3449..b08d13e60 100644
--- a/src/ast/sls/sls_seq_plugin.h
+++ b/src/ast/sls/sls_seq_plugin.h
@@ -122,6 +122,7 @@ namespace sls {
         unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b);
         unsigned edit_distance(zstring const& a, zstring const& b);
         void add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
+        void add_edit_updates2(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
 
         // regex functionality