java-smt

java-smt copied to clipboard

Problems with common SMTLIB2 Strings for OpenSMT2 and Bitwuzla

1

Both OpenSMT2 and Bitwuzla need the removal of certain parts of SMTLIB2 Strings before we can parse them. Examples are comments and `set-logic`. This is currently done lazily and incomplete....

baierd

Missing features and/or potential bugs (willing to fix)

3

Hi! I'm in the process (https://github.com/ftsrg/theta/pull/258) of integrating JavaSMT with our Theta model checker. By doing so, I have discovered some pain points of the integration, which I'd like to...

leventeBajczi

ProverEnvironment pop Later, the variable will be incorrectly modified to be invalid argument. Z3

1

## code ```java @Test void push_pop_test() throws InterruptedException{ SolverContext solverContext = SmtSolverUtil.solverContext(); FormulaManager formulaManager = solverContext.getFormulaManager(); ProverEnvironment prover = SmtSolverUtil.prover(solverContext); IntegerFormulaManager integerFormulaManager = formulaManager.getIntegerFormulaManager(); // constraint: F1>=10 NumeralFormula.IntegerFormula integerFormula =...

yupengj

Improve CI coverage for more systems like MacOS and Windows

1

Our Gitlab-Ci and our AppVeyor CI are good, run well and cover most internal use cases. However, those CIs have limited resources and do not provide more architectures, such as...

kfriedberger

Maven via Github-Maven-Registry instead of OSS-Nexus

4

There are several Maven providers. Currently the first pushed provider is OSS-Nexus, that was integrated long time back. It lacks documentation for new users/admins and is not really nice to...

kfriedberger

We currently depend on several manual steps when publishing a release. We should automate more parts of it. Current steps: - download and build JavaSMT (on Ubuntu 22.04 using prepared...

kfriedberger

Add support for Strings and Rationals to the Princess backend

1

Hello everyone, the goal of this pull request is to add two more theories for strings and rational numbers to the Princess backend. It is a continuation of the work...

daniel-raffler

#380 support multiple architectures for solver binaries z3

6

This branch / pull request exists for tracking some steps towards supporting multiple architectures. I will use Z3 as example, because it was requested several times. Some explanation can be...

kfriedberger

Improve Documentation of Non-Trivial Operations

3

Some operations in SMTLib2, for example Integer `modulo()` and BV `smodulo()` (signed modulo), behave differently. Our documentation does not reflect this properly or fails to explain the differences in a...

baierd

Yices2 produces invalid SMTLIB output when dumping formulas

4

Hello everyone, yices2 does not apply correct quotes while dumping SMTLIB formulas. An example for this can be seen in [VariableNamesTest.testBoolVariableDump()](https://github.com/sosy-lab/java-smt/blob/fed0e55e44243a26cc0ca00b90d6835aef6e5d55/src/org/sosy_lab/java_smt/test/VariableNamesTest.java#L557) where the formula for a (boolean) variable named "("...

daniel-raffler