Search results

NativeLibraries.loadLibrary fails on some systems (fix suggestion included)

Status: Open.

#592 In sosy-lab/java-smt;

· ThomasHaas opened on Jan 30, 2026

Fix Floating-Points for Z3Legacy and Enable Z3Legacy Floating-Point Tests

Z3LegacyOld Z3 version with interpolation supportOld Z3 version with interpolation support

Status: Open.

Bug

#587 In sosy-lab/java-smt;

· baierd opened on Jan 20, 2026

Issues with Ufs that take no arguments

Bitwuzla

CVC5

Princess

Status: Open.

#575 In sosy-lab/java-smt;

· daniel-raffler opened on Jan 5, 2026

Princess: Handle String Literals in Evaluation of Partial Model

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

Princess

Status: Open.

#565 In sosy-lab/java-smt;

· kfriedberger opened on Dec 24, 2025

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

Z3 Invalid Dumping of Quantified Formulas

SMTLIB2

solver

Z3

Status: Open.

Bug

#533 In sosy-lab/java-smt;

· baierd opened on Oct 13, 2025

Constant array values in the model

enhancement

model

Status: Open.

#525 In sosy-lab/java-smt;

· daniel-raffler opened on Sep 13, 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

Irrational numbers in Z3

Z3

Status: Open.

#496 In sosy-lab/java-smt;

· daniel-raffler opened on Jul 26, 2025

Yices2 Parser Problems

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

Yices2

Status: Open.

#488 In sosy-lab/java-smt;

· baierd opened on May 27, 2025