From d5779a6993988b7c167817b91d3b26f2e7ee94ea Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 6 Jun 2026 13:26:01 -0700
Subject: [PATCH] sls_seq_plugin: remove hard aborts in `is_sat` for `str.len`
 and `seq.last_indexof` (#9736)

`src/ast/sls/sls_seq_plugin.cpp::is_sat()` had two unconditional abort
paths (`VERIFY(false)` and `NOT_IMPLEMENTED_YET()`) reachable from valid
string formulas under SLS. This changes those paths to graceful
repair/fail behavior so SLS can continue search instead of terminating
the process.

- **Length coherence fallback no longer aborts**
- Replaced the terminal `VERIFY(false)` in the `str.len` coherence block
with a normal `return false` repair failure path.
- Effect: failed local repair is propagated to the outer SLS loop
instead of crashing.

- **Implemented `seq.last_indexof` coherence handling**
  - Replaced `NOT_IMPLEMENTED_YET()` with concrete coherence logic:
    - read current `x`, `y`, and `e`,
    - compute `actual = sx.last_indexof(sy)`,
    - update `e` when `e != actual`,
    - otherwise continue.
- Effect: formulas containing `seq.last_indexof` are handled in SLS
coherence checks instead of aborting.

- **No new hard-abort behavior introduced**
- In the new `last_index` block, non-numeral `e` is handled by graceful
`return false` (repair failure), not assertion abort.

```cpp
if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) {
    auto sx = strval0(x), 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;
}
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/sls/sls_seq_plugin.cpp | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

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);