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

[github-actions[bot]]

Executive Summary

Note: This analysis ran against the Z3Prover/z3 repository's open issues. Due to a content integrity policy that restricts reading of untrusted user-submitted content, only issues from repository collaborators and automated bots were fully readable. The analysis below covers the 8 fully-accessible open issues plus context from open pull requests and recent commits.

• Total open issues fully analyzed: 8 (collaborator/bot-authored; majority filtered by integrity policy)
• Issues recommended for closure: 0
• Potential duplicates / merge candidates: 0
• Issues with suggested fixes: 2
• Issues commented on: 1
• Automated issues (agentic workflows): 6 (3 agentic-workflow failures + 3 tactic-to-simplifier enhancements)

---

Issues Recommended for Closure

None with high confidence from the issues accessible in this run.

---

Potential Duplicates / Merge Candidates

None identified in the accessible subset.

---

Issues with Suggested Fixes

#9058 — nseq diverging on trivial example

• Component: c3 branch string solver (new nseq/Nielsen solver)
• Relevant source files: src/smt/theory_nseq.cpp, src/smt/theory_nseq.h, src/smt/nseq_context_solver.h, src/smt/seq/ (c3 branch)
• Assigned to: @CEisenhofer, @Copilot
• Age: 16 days (opened 2026-03-20)
• Suggested fix direction: nielsen_graph::generate_extensions encounters str.at atoms introduced by the rewriter (not present in original input) and enters an infinite loop because it doesn't recognize them as already-axiomatized Skolem constants. The fix should either: (1) detect str.at terms in the extension generator and treat them as opaque/axiomatized, or (2) ensure str.at atoms are eagerly reduced before they reach the Nielsen graph phase. The issue includes two SMTLib test cases — one expected sat, one expected unsat — both should be verified after the fix.

---

#7538 — produce-unsat-cores affects convergence

• Component: SMT solver, quantifier reasoning (MBQI)
• Relevant source files: src/smt/smt_context.cpp, src/smt/smt_quantifier.cpp, src/smt/smt_model_checker.cpp, src/smt/smt_params.h
• Assigned to: (nobody)
• Age: 431 days (opened 2025-01-29) ⚠️ Long-standing unaddressed issue
• Suggested fix direction: Two separate problems are reported:
  1. Enabling :produce-unsat-cores true changes the result from unsat to unknown (incomplete quantifiers) with :smt.mbqi false. This suggests that the unsat-core tracking mode disables or changes some inference path. Likely the core tracking interferes with the incomplete-quantifier marking logic in smt_context or changes how the model checker / quantifier solver is invoked.
  2. Trying to disable produce-unsat-cores after it has been set is silently a no-op. This should at minimum emit a warning. The relevant option-setting code is likely in src/cmd_context/cmd_context.cpp or src/smt/smt_context.cpp.
  • A comment was added to this issue (see below).

---

Issues Needing More Information

Issue	Title	Missing Information
#9058	nseq diverging on trivial example	Whether the PR on the c3 branch has already addressed this; issue is assigned but no comments

---

Notable Issues Deserving Attention

Issue	Title	Age	Notes
#7538	produce-unsat-cores affects convergence	431 days	No assignee, no comments; long-standing with a clear reproducer and two separate problems
#9058	nseq diverging on trivial example	16 days	Active c3 branch bug, assigned; has a clear reproducer

---

Agentic Workflow Issues (for context)

These are automated issues from workflow failures that expire 2026-04-11:

Issue	Title	Expires
#9224	Clang Static Analyzer (CSA) Report failed	2026-04-11
#9225	ZIPT String Solver Benchmark failed	2026-04-11
#9226	Ostrich Benchmark: Z3 c3 branch vs ZIPT failed	2026-04-11

These should be assigned to Copilot to debug.

---

Tactic-to-Simplifier Enhancement Issues (for context)

These are bot-created enhancement proposals for the tactic pipeline:

Issue	Title
#9229	Convert tactic nnf to a simplifier
#9230	Convert tactic fpa2bv to a simplifier
#9231	Convert tactic normalize-bounds to a simplifier

Each has a detailed implementation plan including proposed .h file contents and CMakeLists.txt changes.

---

Open PRs Awaiting Merge (for maintainers)

Several open PRs have been open since March 2026 and may need review/merge:

PR	Title	Notes
#9228	Fix missing invalidation of LP changed-bounds set on pop	Assigned levnach, Copilot
#9221	Fix push/pop scopes leaking learned clauses into subsequent proofs	Assigned NikolajBjorner, Copilot
#9222	fstar: formalize FPA rewriter rules from PR #9038 in F*	Assigned NikolajBjorner, Copilot
#9038	Fix #8185: add FPA rewriter simplifications for fma with zero multiplier	Fixes issue #8185
#9028	Fix FPA soundness issue in incremental solving with push/pop	Assigned levnach, Copilot
#9027	Fix Java UnsatisfiedLinkError on macOS (#7640)	Fixes issue #7640

---

Analysis Limitations

The integrity policy prevented reading most user-submitted issues. Only issues authored by repository collaborators (COLLABORATOR/MEMBER) or bots passed the integrity check. A full backlog sweep requires either running this workflow with a higher-trust token or manually triaging user-submitted issues.

---

Automated by Issue Backlog Processor · 2026-04-05

AI generated by Issue Backlog Processor · history

• expires on Apr 12, 2026, 12:26 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9243.