Search results

Add Proof Support to API

API

Basicimpl

CVC4

CVC5

enhancement

MathSAT

OpenSMT2

Princess

SMTInterpol

Z3

Status: Open.

Feature

#558 In sosy-lab/java-smt;

· baierd opened on Dec 11, 2025

·  

Release after 6.0.0

Bitwuzla Parsing Symbols Twice With Error

Bitwuzla

bug

solver

Status: Open.

Bug

#545 In sosy-lab/java-smt;

· baierd opened on Nov 2, 2025

Multi-Dimensional Array Solving and Models Broken for CVC4, Yices2, Bitwuzla, Boolector, and Princess

Bitwuzla

bug

CVC4

Princess

solver

Yices2

Status: Open.

Bug

#538 In sosy-lab/java-smt;

· baierd opened on Oct 28, 2025

Z3 JNI library fails to load in Eclipse PDE environment

Z3

Status: Open.

#537 In sosy-lab/java-smt;

· gravemalte opened on Oct 28, 2025

Z3 Invalid Dumping of Quantified Formulas

SMTLIB2

solver

Z3

Status: Open.

Bug

#533 In sosy-lab/java-smt;

· baierd opened on Oct 13, 2025

Temporary input file "cadical"

bug

Status: Open.

#529 In sosy-lab/java-smt;

· kfriedberger opened on Sep 26, 2025

Constant array values in the model

Status: Open.

#525 In sosy-lab/java-smt;

· daniel-raffler opened on Sep 13, 2025

Add support for arrays with multiple indices in the Princess model

bug

Princess

Status: Open.

#520 In sosy-lab/java-smt;

· daniel-raffler opened on Sep 9, 2025

CI deploys API documentation from branches

dependenciesPull requests that update a dependency filePull requests that update a dependency file

enhancement

Status: Open.

#511 In sosy-lab/java-smt;

· PhilippWendler opened on Sep 1, 2025

IEEE Floating-point to Bitvector Conversion Not Supported in All Solvers

Basicimpl

Bitwuzla

Blocked by Solver Supportsolver does not yet support this feature OR there was not yet any public release of the solversolver does not yet support this feature OR there was not yet any public release of the solver

CVC5

Status: Open.

Feature

#504 In sosy-lab/java-smt;

· baierd opened on Aug 8, 2025

NoSuchElementException for MathSAT5 Model Despite Its Iterator Claiming That There Should Be an Element

bug

MathSAT

Status: Open.

#503 In sosy-lab/java-smt;

· baierd opened on Aug 6, 2025

Irrational numbers in Z3

Z3

Status: Open.

#496 In sosy-lab/java-smt;

· daniel-raffler opened on Jul 26, 2025