Search results

Memory corruption on Mac version of 4.12.5

Status: Open.

#8057 In Z3Prover/z3;

· parno opened on Dec 1, 2025

Unsat only with unnecessary asserts, else unknown

Status: Open.

#8052 In Z3Prover/z3;

· ThomasMayerl opened on Nov 28, 2025

Incorrect response for get-unsat-assumptions

Status: Open.

#8045 In Z3Prover/z3;

· leeabarnett opened on Nov 25, 2025

Incorrect 'unknown' results after using Z3_solver_translate in multiple threads

Status: Open.

#8035 In Z3Prover/z3;

· toolCHAINZ opened on Nov 18, 2025

Soundness issue in string logic

Status: Open.

#8023 In Z3Prover/z3;

· wintered opened on Nov 14, 2025

Massive performance regression in 4.15.4.0 apparently due to lock contention

Status: Open.

#8019 In Z3Prover/z3;

· emeryberger opened on Nov 12, 2025

BLD: provide CMake option to install only python bindings

Status: Open.

#8016 In Z3Prover/z3;

· h-vetinari opened on Nov 7, 2025

Infinite loop/performance regression in Z3 4.15.3

Status: Open.

#7991 In Z3Prover/z3;

· rod-chapman opened on Oct 18, 2025

Wrong verdict with <code>(set-option :sat.smt true)</code>

Status: Open.

#7990 In Z3Prover/z3;

· ThomasHaas opened on Oct 18, 2025

Z3 4.15.3 is not on opam

Status: Open.

#7958 In Z3Prover/z3;

· Lysxia opened on Oct 2, 2025

z3 behavior depends on the names of the functions

Status: Open.

#7957 In Z3Prover/z3;

· mikulas-patocka opened on Oct 1, 2025

Another seemingly infinite loop

Status: Open.

#7951 In Z3Prover/z3;

· mtzguido opened on Sep 29, 2025