Search results

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

Potential correctness issue in integer arithmetic optimization

Status: Open.

#7641 In Z3Prover/z3;

· merlinsun opened on May 9, 2025

java.lang.UnsatisfiedLinkError at MacOS with JavaExample.java

Status: Open.

#7640 In Z3Prover/z3;

· sabrieker opened on May 8, 2025

Performance regression when using Fixedpoint solver (from 4.13.2 to 4.14.1)

Status: Open.

#7632 In Z3Prover/z3;

· KihongHeo opened on Apr 24, 2025

Add support for Algebraic Datatypes in js bindings

javascriptPull requests that update Javascript codePull requests that update Javascript code

Status: Open.

#7621 In Z3Prover/z3;

· NikolajBjorner opened on Apr 14, 2025

Spacer unsoundness regarding CHCs involving inductively defined datatypes

Horn

Status: Open.

#7611 In Z3Prover/z3;

· coord-e opened on Apr 5, 2025