Search results

[code-simplifier] Simplify int_cube: remove goto, use aggregate/brace init

agentic-workflows

automation

code-quality

refactoring

Status: Open.

#9866 In Z3Prover/z3;

· github-actions opened on Jun 15, 2026

.NET wrapper is tagged x64-only, blocking arm64 .NET hosts despite arm64 native libraries being shipped

Status: Open.

#9863 In Z3Prover/z3;

· taol-assignments opened on Jun 15, 2026

Historical nlsat regression tests still rely on print-only diagnostics

Status: Open.

#9859 In Z3Prover/z3;

· peter941221 opened on Jun 14, 2026

lia2card drops a bounded equality that still flows through a recfun definition

Status: Open.

#9855 In Z3Prover/z3;

· peter941221 opened on Jun 14, 2026

Z3 times out on failing proof, hoped to get sat.

Status: Open.

#9843 In Z3Prover/z3;

· davedets opened on Jun 12, 2026

Smart constructors for regex ranges: emptiness check + Boolean-connective reduction at construction time

Status: Open.

#9813 In Z3Prover/z3;

· veanes opened on Jun 10, 2026

More issues with constant arrays and z3 reporting sat instead of unsat

Status: Open.

#9705 In Z3Prover/z3;

· mpreiner opened on Jun 3, 2026

z3 returns invalid model for formula involving seq.map

Status: Open.

#9642 In Z3Prover/z3;

· ryanfanchiotti opened on May 27, 2026

z3 returns sat on unsat formula involving seq.fold_left

Status: Open.

#9602 In Z3Prover/z3;

· ryanfanchiotti opened on May 23, 2026

FetchContent documentation incomplete, it seems.

Status: Open.

#9598 In Z3Prover/z3;

· davedets opened on May 22, 2026

Spacer returns sat with an invalid model for an unsat CHC over ADTs

Status: Open.

#9583 In Z3Prover/z3;

· naokikob opened on May 21, 2026

z3 hangs on constraint with mod

Status: Open.

#9509 In Z3Prover/z3;

· ranjitjhala opened on May 12, 2026