Z3Prover: proyectos de código abierto

z3.py omits additional domains of multidimensional arrays during printing Abierto

Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100

Z3Prover/z3#10889 · Abierto el 21/9/2026

MBQI cannot solve goals equating a canonicalised free array with a lambda: (= (lambda (x) (ite (G x) (select f x) d)) (lambda (x) (ite (G x) (t x) d))) stays unknown/timeout Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 38/100

Z3Prover/z3#10886 · 1 comentario · Abierto el 21/9/2026

False `unsat` for inexact symbolic Real-to-binary64 rounding Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

Z3Prover/z3#10881 · 1 reacción · 2 asignados · Abierto el 20/9/2026

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

Z3Prover/z3#10863 · 1 reacción · 3 asignados · Abierto el 19/9/2026

Could we have a new release on nuget.org? Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#10711 · 2 comentarios · Abierto el 1/9/2026

SIGSEGV inside the MBQI model checker's auxiliary `context::check` — fault site varies per run (looks like state corruption); regression, 4.16.0 is clean Abierto

Z3Prover/z3#10385 · 10 comentarios · 2 asignados · Abierto el 4/8/2026

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

Floats

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

Z3Prover/z3#10176 · 1 comentario · Abierto el 21/7/2026

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

Floats

Z3Prover/z3#9953 · 1 reacción · 2 asignados · Abierto el 25/6/2026

Consolidated invalid model bugs Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

Z3Prover/z3#9319 · 12 comentarios · Abierto el 16/4/2026

Is there a way to combine QF_BV and QF_IDL? Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#8940 · 7 comentarios · Abierto el 11/3/2026

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

Z3Prover/z3#8194 · 4 comentarios · 1 reacción · 2 asignados · Abierto el 14/1/2026

Unsat only with unnecessary asserts, else unknown Abierto

Floats

Z3Prover/z3#8052 · 1 reacción · 2 asignados · Abierto el 28/11/2025

Infinite loop/performance regression in Z3 4.15.3 Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#7991 · 14 comentarios · 1 reacción · Abierto el 18/10/2025

Incorrect model Abierto

Floats

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

Z3Prover/z3#7842 · 7 comentarios · Abierto el 2/9/2025

Observe both compute and memory regression when upgrade to 4.15.3 from 4.14.1 Abierto

string

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

Z3Prover/z3#7800 · 2 comentarios · Abierto el 19/8/2025

Memory and time blow-up with z3 4.15.2 Abierto

Z3Prover/z3#7735 · 5 comentarios · 1 reacción · 1 asignado · Abierto el 15/7/2025

Spacer returns `sat` instead of expected `unsat`, and fails model validation on a specific input Abierto

Horn

Z3Prover/z3#7730 · 2 comentarios · 1 asignado · Abierto el 12/7/2025

invalid model Abierto

API usability / compile bug string

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

Z3Prover/z3#7664 · 1 comentario · Abierto el 28/5/2025

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

Horn

Z3Prover/z3#7632 · 2 comentarios · 1 asignado · Abierto el 24/4/2025

PartialOrder hangs when reasoning about bottom element Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

Z3Prover/z3#7592 · 1 comentario · Abierto el 20/3/2025

Slow unsat multiplication overflow solving Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#7526 · 1 comentario · Abierto el 23/1/2025

Invalid model issue on float formula Abierto

Floats

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

Z3Prover/z3#7431 · Abierto el 22/10/2024

Spacer: Timeout with simple array example Abierto

Horn

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#7425 · 5 comentarios · Abierto el 18/10/2024

Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers Abierto

Z3Prover/z3#7238 · 1 comentario · 1 reacción · 2 asignados · Abierto el 29/5/2024

TransitiveClosure + Quantifiers extremely slow Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#7167 · 1 comentario · Abierto el 16/3/2024

[consolidated] hang on small instances (string, bit-vector) Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

Z3Prover/z3#7164 · 11 comentarios · Abierto el 14/3/2024

Unknown when working with String Sequences Abierto

string

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

Z3Prover/z3#7151 · 2 reacciones · Abierto el 6/3/2024

Finite sets Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

Z3Prover/z3#6788 · 3 comentarios · Abierto el 27/6/2023

Invalid interpretations produced by Spacer Abierto

Horn

Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

Z3Prover/z3#6716 · 4 comentarios · Abierto el 9/5/2023

Performance regression issue on string Abierto

string

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

Z3Prover/z3#6668 · Abierto el 3/4/2023

Unexpected code reached in Spacer Abierto

Horn

Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

Z3Prover/z3#6122 · 6 comentarios · Abierto el 30/6/2022

Issues with models of Horn clauses Abierto

Horn

Dificultad 5/5 Más de una semana Aptitud para principiantes 15/100

Z3Prover/z3#5920 · 4 comentarios · Abierto el 23/3/2022

Performance regression from 4.8.7.0 to 4.8.8.0 and all later versions. Abierto

string

Z3Prover/z3#5763 · 1 reacción · 2 asignados · Abierto el 10/1/2022

Longer proofs with recent versions of Z3 Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

Z3Prover/z3#5395 · 6 comentarios · Abierto el 9/7/2021

proof regressions from 4.8.8 to 4.8.9 and current master Abierto

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

Z3Prover/z3#4746 · 7 comentarios · Abierto el 21/10/2020

Spacer nondeterminism Abierto

Horn

Z3Prover/z3#4407 · 13 comentarios · 1 asignado · Abierto el 20/5/2020

Spacer: error "query failed: Uninterpreted 'mod' in <null> Abierto

Horn

Z3Prover/z3#3962 · 15 comentarios · 1 asignado · Abierto el 14/4/2020

`unsat` sequence benchmark, now can't be handled by z3 Abierto

string

Z3Prover/z3#3508 · 1 comentario · 1 asignado · Abierto el 25/3/2020

Long strings timeout Abierto

performance string

Dificultad 5/5 Más de una semana Aptitud para principiantes 20/100

Z3Prover/z3#2364 · 1 comentario · Abierto el 25/6/2019

Spacer's difficulty in finding linear invariants Abierto

Horn

Z3Prover/z3#2278 · 2 comentarios · 1 asignado · Abierto el 13/5/2019

Quantified BV formula, significant performance regression Abierto

Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

Z3Prover/z3#2075 · 8 comentarios · Abierto el 8/1/2019

str.at is this a bug? Abierto

string

Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

Z3Prover/z3#1628 · 1 comentario · Abierto el 18/5/2018

infinite loop making model for recursive datatype in presence of quantifiers Abierto

enhancement

Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

Z3Prover/z3#578 · 6 comentarios · Abierto el 28/4/2016

Z3Prover

Recibe los nuevos issues en tu correo