[Issue Backlog] Backlog Analysis - 2026-06-07

[github-actions[bot]]

Issue Backlog Analysis - 2026-06-07

Executive Summary

• Total open issues analyzed: 2 new (+ 4 visible but previously processed)
• Issues recommended for closure: 0
• Potential duplicates / merge candidates: 0
• Issues with confirmed bugs / suggested fixes: 2
• Issues commented on: 1
• Integrity policy note: 26 of 30 issues per page are filtered; only approved-contributor issues are accessible

---

New Issues Since Last Run (Batch Cursor: #9713 → #9738)

#9726 — sls_seq_plugin: wrong index in edit_distance_with_updates can_add check

• Component: SLS (Stochastic Local Search) string solver — src/ast/sls/sls_seq_plugin.cpp
• Type: Bug — wrong index in edit_distance_with_updates
• Status: CONFIRMED via source inspection
• Relevant source file: src/ast/sls/sls_seq_plugin.cpp, line 915
• Bug: The guard b.can_add(i - 1) uses the i index (which iterates over string a) instead of j (which iterates over string b). The correct code in the update-generation block directly below uses b.can_add(j - 1), confirming the bug by contrast.

// Current (BUG) - line 915:
if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) {
// Correct:
if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {

• Impact: When i != j, the mutability cost matrix u is computed incorrectly, causing flawed string repair proposals in the SLS solver. The bug is masked when i == j (square sub-problems).
• Suggested fix direction: Change i - 1 to j - 1 on line 915 of sls_seq_plugin.cpp.

---

#9738 — euf_sgraph.cpp: drop_left/drop_right O(count×depth) vs O(depth) + classify double is_string call

• Component: ZIPT string solver port — src/ast/euf/euf_sgraph.cpp (on branch copilot/fix-euf-snode-support only; not yet on main)
• Type: Performance improvement + code quality
• Status: Valid, well-documented. Files don't exist on main yet.
• Improvements identified:
  1. drop_left/drop_right use O(count × depth) loop instead of O(depth) recursive tree navigation
  2. classify calls is_string twice when one call suffices
  3. Future opportunity: add per-node DropLeftCache/DropRightCache for O(1) amortized cost

---

Issues with Suggested Fixes

Issue	Title	Component	Fix Complexity
#9726	sls_seq_plugin: wrong index in edit_distance_with_updates	SLS string solver	Trivial (1 char)
#9738	euf_sgraph.cpp: drop_left/drop_right O(count×depth)	ZIPT port (feature branch)	Moderate

---

Notable Open PRs Awaiting Review

PR	Title	Age	Notes
#9591	Fix #9171: add expand-records preprocessing	17 days	89/90 tests pass; awaiting @NikolajBjorner review
#9027	Fix Java UnsatisfiedLinkError on macOS (#7640)	long-standing	Still open
#9038	fix #8185: add FPA rewriter simplifications	long-standing	Still open

---

Issues Recommended for Closure

None identified this run.

---

Potential Duplicates / Merge Candidates

None new. Previously identified clusters remain (see prior runs):

• Infinite loop/performance regression in Z3 4.15.3 #7991, Memory and time blow-up with z3 4.15.2 #7735, Z3 4.8.14 concludes input file is unsat, but loops forever on 4.15.1 #7700: infinite loop/memory blow-up in Z3 4.15.x
• Incorrect model for QF_SLIA #7841, invalid model #7664, invalid model issue on an incremental QF_SLIA formula #6982: invalid models in QF_SLIA string theory
• Spacer returns sat instead of expected unsat, and fails model validation on a specific input #7730, Spacer unsoundness regarding CHCs involving inductively defined datatypes #7611, Soundness bug in HORN logic #4008, z3 returning wrong sat-answer #7417: Spacer soundness cluster

---

Notes

• The integrity policy continues to filter ~87% of issues per page; only issues from approved contributors (NikolajBjorner, nunoplopes, mtzguido) are visible.
• Issue [zipt-review] sls_seq_plugin: wrong index in edit_distance_with_updates can_add check #9726 contains a verified, patch-ready one-character bug fix in the SLS string solver.
• Issue [zipt-review] euf_sgraph.cpp: drop_left/drop_right O(count×depth) vs O(depth) + classify double is_string call #9738 applies to the copilot/fix-euf-snode-support feature branch, not main.
• PR Fix #9171: add expand-records preprocessing to enable constant folding #9591 (fixes the long-standing Regression in a constant-folding example #9171 divergence bug) has been awaiting review for 17 days with 89/90 tests passing.

---

Automated by Issue Backlog Processor — runs every 2 days

Generated by Issue Backlog Processor · sonnet46 1.4M · ◷

• expires on Jun 14, 2026, 12:39 AM UTC

[github-actions[bot]]

This discussion has been marked as outdated by Issue Backlog Processor.

A newer discussion is available at Discussion #9778.