Search results

[aw] QF_S String Solver Benchmark failed

agentic-workflows

Status: Open.

#9470 In Z3Prover/z3;

· github-actions opened on May 6, 2026

Z3 Bug Report: sat.smt=true returns invalid model for QF_UFBV formulas with boolean-valued UF predicates

Status: Open.

#9469 In Z3Prover/z3;

· programsurf opened on May 6, 2026

[aw] Code Simplifier failed

agentic-workflows

Status: Open.

#9468 In Z3Prover/z3;

· github-actions opened on May 5, 2026

[aw] API Coherence Checker failed

agentic-workflows

Status: Open.

#9467 In Z3Prover/z3;

· github-actions opened on May 5, 2026

[aw] ZIPT Code Reviewer failed

agentic-workflows

Status: Open.

#9466 In Z3Prover/z3;

· github-actions opened on May 5, 2026

sat.smt=true returns invalid model for BV comparator assertions (smt.elim_unconstrained interaction)

Status: Open.

#9463 In Z3Prover/z3;

· programsurf opened on May 5, 2026

Consolidated invalid model bugs

Status: Open.

#9319 In Z3Prover/z3;

· lmaltsis opened on Apr 16, 2026

apply qe on a small BV formula does not produce output within 60s

Status: Open.

#9315 In Z3Prover/z3;

· jwimd opened on Apr 16, 2026

Z3 4.15.3 instability on identical input across macOS and Linux

Status: Open.

#9311 In Z3Prover/z3;

· rod-chapman opened on Apr 15, 2026

push/pop scopes affect performance of subsequent proofs

Status: Open.

#9220 In Z3Prover/z3;

· davedets opened on Apr 3, 2026

Regression in a constant-folding example

Status: Open.

#9171 In Z3Prover/z3;

· LeventErkok opened on Mar 30, 2026

Soundness bug(s) in nonlinear solver

Status: Open.

#9139 In Z3Prover/z3;

· wintered opened on Mar 26, 2026