Search results

Spacer returns <code>sat</code> instead of expected <code>unsat</code>, and fails model validation on a specific input

Status: Open.

#7730 In Z3Prover/z3;

· coeff-aij opened on Jul 12, 2025

JS (High-level) - Eventual memory corruption

Status: Open.

#7723 In Z3Prover/z3;

· AiBobby opened on Jul 7, 2025

Add Z3 to the Bazel Central Registry (BCR)

Status: Open.

#7720 In Z3Prover/z3;

· smolkaj opened on Jul 3, 2025

Z3 4.8.14 concludes input file is <code>unsat</code>, but loops forever on 4.15.1

performanceIssues that relate primarily to the performance of Z3, such as timeoutsIssues that relate primarily to the performance of Z3, such as timeouts

Status: Open.

#7700 In Z3Prover/z3;

· RyanGlScott opened on Jun 27, 2025

Convergence regression when migrating from 4.13.3 to 4.15.2

bug

performanceIssues that relate primarily to the performance of Z3, such as timeoutsIssues that relate primarily to the performance of Z3, such as timeouts

question

Status: Open.

#7697 In Z3Prover/z3;

· etiennejf opened on Jun 27, 2025

Inconsistent results in CLI and Z3Py API

API usability / compile

bug

no-repro

Status: Open.

#7687 In Z3Prover/z3;

· izycheva opened on Jun 17, 2025

OCaml bindings don't install with cmake build system

build/releasebuild and release scripts and processbuild and release scripts and process

Status: Open.

#7684 In Z3Prover/z3;

· numinit opened on Jun 15, 2025

Potential issue in arithmetic optimization

Arithmetic

bug

Status: Open.

#7677 In Z3Prover/z3;

· merlinsun opened on Jun 11, 2025

invalid model

API usability / compile

bug

string

Status: Open.

#7664 In Z3Prover/z3;

· LeventErkok opened on May 28, 2025

z3 model that doesn't satisfy all given constraints

bug

build/releasebuild and release scripts and processbuild and release scripts and process

DebugDebug branch issuesDebug branch issues

Status: Open.

#7658 In Z3Prover/z3;

· dan-simon opened on May 22, 2025

Linker errors during Julia bindings

Status: Open.

#7644 In Z3Prover/z3;

· songkomkrit opened on May 12, 2025

Z3 goes to an infinite loop on a theorem on parity of n*(n+1)

Status: Open.

#7643 In Z3Prover/z3;

· amigalemming opened on May 9, 2025