Search results

Incorrect model for Real-to-FP32-to-Real conversion

Floats

Status: Open.

#10176 In Z3Prover/z3;

· wingsyuyi-satori opened on Jul 21, 2026

Solution soundness issue in QF_FP

Floats

Status: Open.

#10175 In Z3Prover/z3;

· wintered opened on Jul 21, 2026

qe2 leaves a fresh undeclared constant (from the eliminated variable) in the quantifier-eliminated result

Status: Open.

#10172 In Z3Prover/z3;

· daniel-larraz opened on Jul 21, 2026

Linker errors when building Z3-5.0.0 on Windows using mingw-w64-ucrt-x86_64-gcc

Status: Open.

#10171 In Z3Prover/z3;

· RyanGlScott opened on Jul 21, 2026

qe2 introduces a non-linear term (a product of two variables) when eliminating quantifiers from a linear (LIA) formula

Status: Open.

#10170 In Z3Prover/z3;

· daniel-larraz 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

Floats

Status: Open.

#10162 In Z3Prover/z3;

· Zac-HD 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