Search results

Incorrect model with smt.bv.solver=2 and an unused define-fun

Status: Open.

#10168 In Z3Prover/z3;

· wingsyuyi-satori opened on Jul 20, 2026

smt-lib compliance turns unsat to unknown (with a bizarre unknown message)

Status: Open.

#10166 In Z3Prover/z3;

· LeventErkok opened on Jul 19, 2026

unknown on trivially valid goals over to_fp(to_real(x)). Every assignment is a model, but Z3 finds none

Status: Open.

#10162 In Z3Prover/z3;

· Zac-HD opened on Jul 18, 2026

5.0.0 parallel mode returns unknown ("sat.max.conflicts") in ~1s on hard QF_BV — reason-string mismatch skips the cube conflict-budget escalation

Status: Open.

#10161 In Z3Prover/z3;

· ChaiTRex opened on Jul 18, 2026

Parallel solver writes the bare reason_unknown string to stderr at verbosity 0 (parallel_tactical.cpp:2186)

Status: Open.

#10160 In Z3Prover/z3;

· ChaiTRex opened on Jul 18, 2026

[Refutational Soundness Bug] Incorrect UNSAT in Float32 FP/Real round-trip arithmetic.

Floats

Status: Open.

#9953 In Z3Prover/z3;

· wingsyuyi-satori opened on Jun 25, 2026

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

bug

Status: Open.

#9705 In Z3Prover/z3;

· mpreiner opened on Jun 3, 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

qe

Status: Open.

#9315 In Z3Prover/z3;

· jwimd opened on Apr 16, 2026

Installing Z3 via opam on Windows PowerShell with Cygwin requires cl

Status: Open.

#9133 In Z3Prover/z3;

· LaifsV1 opened on Mar 26, 2026

Free variable in the model

Status: Open.

#9063 In Z3Prover/z3;

· LeventErkok opened on Mar 20, 2026

Python installation on ARM64 doesn't work on M3

Status: Open.

#9056 In Z3Prover/z3;

· izycheva opened on Mar 20, 2026