Search results

Soundness issue in Real (seemingly unrelated to Float)

Status: Open.

#8397 In Z3Prover/z3;

· wintered opened on Jan 27, 2026

Z3 segfaults instead of erroring out when passing the wrong type parameters to Z3.Datatype.mk_sort_ref_p

Status: Open.

#8376 In Z3Prover/z3;

· mben-romdhane opened on Jan 27, 2026

Expose an API function to allow defining polymorphic recursive datatypes

Status: Open.

#8375 In Z3Prover/z3;

· mben-romdhane opened on Jan 27, 2026

[Conventions] Refactor dyn_ack.cpp to use C++17 structured bindings for app_pair/app_triple

automated

code-quality

enhancement

Status: Open.

#8353 In Z3Prover/z3;

· github-actions opened on Jan 27, 2026

Soundness issue by converting from bit representation to fp to Real

Floats

Status: Open.

#8345 In Z3Prover/z3;

· ThomasMayerl opened on Jan 26, 2026

ASSERTION VIOLATION File: ../src/util/mpzzp.h Line: 139

Status: Open.

#8292 In Z3Prover/z3;

· wingsyuyi-satori opened on Jan 23, 2026

Incorrect model with <code>:produce-proofs true</code> involving String Theory and UF

Status: Open.

#8194 In Z3Prover/z3;

· wingsyuyi-satori opened on Jan 14, 2026

Incorrect model in mixed FP/Real logic triggered by extra string constraint

Floats

Status: Open.

#8185 In Z3Prover/z3;

· wingsyuyi-satori opened on Jan 13, 2026

[Refutational Soundness Bug] Incorrect UNSAT in Real-to-FP conversion with RNE/RNA overflow

Floats

Status: Open.

#8183 In Z3Prover/z3;

· wingsyuyi-satori opened on Jan 13, 2026

Incorrect model with (_ FloatingPoint 2 24) and <code>fp.to_real</code>

Floats

Status: Open.

#8169 In Z3Prover/z3;

· wingsyuyi-satori opened on Jan 12, 2026

Performance degradation in Z3 on QF_SLIA instances with fixed-length strings and prefix/suffix constraints

Status: Open.

#8096 In Z3Prover/z3;

· wingsyuyi-satori opened on Dec 19, 2025

Memory corruption on Mac version of 4.12.5

Status: Open.

#8057 In Z3Prover/z3;

· parno opened on Dec 1, 2025