3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-08 01:50:55 +00:00

sls_seq_plugin: fix breakcontinue in add_substr_edit_updates (#9735)

`add_substr_edit_updates` uses a `HashSet` to deduplicate substrings of
`val_other`, but on a duplicate hit it `break`s the inner loop instead
of skipping just that entry. This causes all longer substrings from the
same starting position to be silently dropped as repair candidates.

## Change

- **`src/ast/sls/sls_seq_plugin.cpp`** — replace `break` with `continue`
in the inner substring-enumeration loop.

```cpp
// Before — exits the inner loop on first duplicate, missing e.g. "ab" in "aab"
if (set.contains(sub))
    break;

// After — skips only the duplicate, continues with longer substrings at same offset
if (set.contains(sub))
    continue;
```

For `val_other = "aab"`, the old code never proposed `"ab"` (i=1, j=2)
as a repair candidate because the duplicate `"a"` (i=1, j=1) terminated
the inner loop prematurely.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-06-06 13:23:44 -07:00 committed by GitHub
parent 69c3b2e5a4
commit 2f280a7baf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -753,7 +753,7 @@ namespace sls {
for (unsigned j = 1; j <= val_other.length() - i; ++j) {
zstring sub = val_other.extract(i, j);
if (set.contains(sub))
break;
continue;
set.insert(sub);
}
}