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

[github-actions[bot]]

Caution

agentic threat detected
Threat detection flagged this output in warn mode. Manual review is REQUIRED before any follow-up automation.

Details

Potential security threats were detected in the agent output.

Review the workflow run logs for details.

Issue Backlog Analysis — 2026-06-05

Executive Summary

• Total open issues analyzed this run: 3 accessible (27 filtered by integrity policy)
• New issues since last run (cursor 9691): 1 ([zipt-review] ZIPT Code Review: Sign bug in seq_offset_eq::find causes missed length-based splits #9713)
• Issues recommended for closure: 0
• Potential duplicates / merge candidates: 0 new
• Issues with suggested fixes: 1 ([zipt-review] ZIPT Code Review: Sign bug in seq_offset_eq::find causes missed length-based splits #9713 — patch ready)
• Issues commented on: 1 ([zipt-review] ZIPT Code Review: Sign bug in seq_offset_eq::find causes missed length-based splits #9713)

Integrity policy note: The workflow's integrity filter continues to restrict issue access to approved contributors only. 27 of 30 issues returned by the API were blocked this run. The 3 accessible issues were #9713 (new), #2046 (prev. processed), #7538 (prev. processed).

---

Issues with Suggested Fixes

#9713 — Sign bug in seq_offset_eq::find causes missed length-based splits

• Component: String solver (src/smt/)
• Relevant source file: src/smt/seq_offset_eq.cpp lines 97–108
• Severity: Completeness / performance (not soundness — wrong offsets cause splits to be skipped, not wrong answers)
• Fix status: ✅ Patch-ready — 2-line change, confirmed correct by code inspection

Root cause: m_offset_equalities uses canonical key order (lower_id, higher_id). len_offset() correctly negates val when keys are swapped at insertion. find() swaps keys for lookup but does not negate on return, so callers receive the wrong sign for ~50% of lookups (whenever root1.id > root2.id). This causes len_based_split to build a literal whose model assignment is l_false, silently skipping the split.

Fix (from the automated ZIPT review in the issue):

-    if (n1->get_owner_id() > n2->get_owner_id())
+    bool swapped = n1->get_owner_id() > n2->get_owner_id();
+    if (swapped)
         std::swap(n1, n2);
 ...
-        return offset;
+        return swapped ? -offset : offset;

---

Issues Recommended for Closure

None with sufficient confidence this run.

---

Potential Duplicates / Merge Candidates

No new duplicates identified this run. Previously identified clusters remain open:

Cluster	Issues	Notes
Memory blow-up in Z3 4.15.x	#7991, #7735, #7700	Likely same root cause
Invalid models in QF_SLIA string theory	#7841, #7664, #6982	Same symptom family
produce-proofs + string constraints	#8185, #8194	Related root cause
Spacer MBP soundness	#7730, #7611, #4008, #7417	Partially addressed by PR #9692

---

Notable Open PRs Awaiting Review

PR	Title	Age	Status
#9591	Fix #9171: add expand-records preprocessing	15 days	Awaiting @NikolajBjorner review; 89/90 tests pass
#9359	Improve qe-light elimination for BV vars	—	Open
#9027	Fix Java UnsatisfiedLinkError on macOS (#7640)	—	Open
#9038	fix #8185: FPA rewriter for fma with zero	—	Open

PR #9591 (fixes #9171) has been awaiting review for 15 days. It addresses a divergence bug on single-constructor algebraic datatype problems.

---

Notable Merged PRs Since Last Run (2026-06-03)

PR	Title	Notes
#9692	Fix MBP QEL soundness bug in datatype accessor elimination	⚠️ Soundness fix: mbp_dt_tg::apply() was incorrectly calling rm_accessor when the model assigns a different constructor, making satisfiable formulas return false
#9697	Handle SIGXCPU like a regular timeout	Z3 now exits cleanly on CPU time limit (ulimit -t) instead of crashing
#9695	Update used_enodes properly	Fixes incorrect trace from PR #9405
#9696	Remove redundant min_gen_match search	Cleanup in euf_mam.cpp, sync with mam.cpp
#9716	Fix quoting in low-level pretty printer	Pretty printer quoting correctness fix
#9709	Cleanup thanks to Copilot	Code cleanup

---

Issues Needing More Information

No new issues needing information this run.

---

Long-Running Open Issues (Selected, from prior runs)

Issue	Title	Age	Notes
#2046	qe2 hangs with trivial problem	~2,700 days	qe2 tactic infinite loop, filed by @nunoplopes
#7538	produce-unsat-cores affects convergence	~490 days	Option affects solver path, filed by @mtzguido
#9171	Divergence on single-constructor ADT benchmark	~90 days	Fix ready in PR #9591, awaiting review

---

Automated by Issue Backlog Processor — runs every 2 days. Run 26 of 26 total runs. Cumulative issues analyzed: 121.

Note

🔒 Integrity filter blocked 27 items

The following items were blocked because they don't meet the GitHub integrity level.

• z3 returns sat on unsat formula involving seq.fold_left #9602 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• More issues with constant arrays and z3 reporting sat instead of unsat #9705 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Z3 does proof when function defined via quantifiers, but fails when defined via define-func-rec. #9473 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Z3 on macOS x86_64 broken since z3 v4.15.4 #9662 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• z3 returns invalid model for formula involving seq.map #9642 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Spacer returns sat with an invalid model for an unsat CHC over ADTs #9583 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• FetchContent documentation incomplete, it seems. #9598 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Regression in a constant-folding example #9171 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• z3 hangs on constraint with mod #9509 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• sat.smt=true returns invalid model for BV comparator assertions (smt.elim_unconstrained interaction) #9463 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• push/pop scopes affect performance of subsequent proofs #9220 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Unable to load shared library 'libz3'  #4780 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Consolidated invalid model bugs #9319 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• Z3 4.15.3 instability on identical input across macOS and Linux #9311 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• apply qe on a small BV formula does not produce output within 60s #9315 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• invalid model #7664 list_issues: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• ... and 11 more items

To allow these resources, lower min-integrity in your GitHub frontmatter:

tools:
  github:
    min-integrity: approved  # merged | approved | unapproved | none

Generated by Issue Backlog Processor · sonnet46 1.3M · ◷

• expires on Jun 12, 2026, 12:45 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9749.