Search results

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

Z3 times out on formula Simplify does quickly

Status: Open.

#9473 In Z3Prover/z3;

· davedets opened on May 6, 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

Installing Z3 via opam on Windows PowerShell with Cygwin requires cl

Status: Open.

#9133 In Z3Prover/z3;

· LaifsV1 opened on Mar 26, 2026

[Python] parallel.threads.max fails to utilize multiple cores concurrently on massive QF_BV programmatic workloads

Status: Open.

#9117 In Z3Prover/z3;

· icebreaker2315 opened on Mar 24, 2026