Search results

"p" as Constant Name Changes Minimize Result

Status: Open.

#8076 In Z3Prover/z3;

· MorfMichael opened on Dec 14, 2025

Request lower glibc baseline on ARM

Status: Open.

#8074 In Z3Prover/z3;

· kurisu6912 opened on Dec 14, 2025

Incorrect array equivalence result

Status: Open.

#8065 In Z3Prover/z3;

· RobinWebbers opened on Dec 11, 2025

Why is maximize_ac_sharing initialized lazily?

Status: Open.

#8062 In Z3Prover/z3;

· CanCebeci opened on Dec 10, 2025

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