All issues

Search results

Move proof canaries to z3test

Status: Open.

#10988 In Z3Prover/z3;

· Nikolaj Bjorner (NikolajBjorner) opened on Sep 30, 2026

Unsound unsat: to_fp from a symbolic Real loses the rounding carry into the next binade (6-line repro)

Floats

Status: Open.

#10931 In Z3Prover/z3;

· headinthebox opened on Sep 27, 2026

False unsat for inexact symbolic Real-to-binary64 rounding

Floats

Status: Open.

#10881 In Z3Prover/z3;

· Dmitriy (mrzv) opened on Sep 20, 2026

Performance regression 4.13.3 -> 4.15.0 and later: quantified UF+LIA query 43x slower (then unsolvable) with smt.case_split 3

Status: Open.

#10863 In Z3Prover/z3;

· Gabriel Ebner (gebner) opened on Sep 19, 2026

Could we have a new release on nuget.org?

Status: Open.

#10711 In Z3Prover/z3;

· Howard van Rooijen (HowardvanRooijen) opened on Sep 1, 2026

[Solution Soundness Bug] Incorrect SAT in Float32 FP/Real round-trip arithmetic.

Floats

Status: Open.

#10176 In Z3Prover/z3;

· wingsyuyi (wingsyuyi-satori) opened on Jul 21, 2026

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

Floats

Status: Open.

#9953 In Z3Prover/z3;

· wingsyuyi (wingsyuyi-satori) opened on Jun 25, 2026

Consolidated invalid model bugs

Status: Open.

#9319 In Z3Prover/z3;

· Lu Maltsis (lmaltsis) opened on Apr 16, 2026

Is there a way to combine QF_BV and QF_IDL?

Status: Open.

#8940 In Z3Prover/z3;

· Thomas Haas (ThomasHaas) opened on Mar 11, 2026

Incorrect model with :produce-proofs true involving String Theory and UF

Status: Open.

#8194 In Z3Prover/z3;

· wingsyuyi (wingsyuyi-satori) opened on Jan 14, 2026

Unsat only with unnecessary asserts, else unknown

Floats

Status: Open.

#8052 In Z3Prover/z3;

· ThomasMayerl opened on Nov 28, 2025

Infinite loop/performance regression in Z3 4.15.3

Status: Open.

#7991 In Z3Prover/z3;

· Roderick Chapman (rod-chapman) opened on Oct 18, 2025