diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index 5563ade51..f516b2948 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -172,9 +172,7 @@ namespace sls {
                     return false;
                 if (r > sx.length() && update(x, sx + zstring(random_char())))
                     return false;
-                // This case seems to imply unsat
-                verbose_stream() << "The input might be unsat\n"; // example to trigger: (assert (and (>= (str.len X) 2) (= (str.substr X 0 1) "")))
-                VERIFY(false);
+                // Both updates failed. Treat as unsatisfied and let outer search continue.
                 return false;
             }
 
@@ -198,8 +196,16 @@ namespace sls {
                 return false;
             }
             if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) {
-                // TODO
-                NOT_IMPLEMENTED_YET();
+                auto sx = strval0(x);
+                auto sy = strval0(y);
+                rational val_e;
+                if (!a.is_numeral(ctx.get_value(e), val_e))
+                    return false;
+                rational actual(sx.last_indexof(sy));
+                if (val_e == actual)
+                    continue;
+                update(e, actual);
+                return false;
             }
             if (seq.str.is_stoi(e, x) && seq.is_string(x->get_sort())) {
                 auto sx = strval0(x);