Baier D.

Long File Names Cause BenchExec to Throw an Error When Processing Run Results

1

The following error and stack-trace was returned after a run has concluded and while the results were collected/processed: ``` Traceback (most recent call last): File "/data/scratch/baier/cpachecker-smg2/scripts/benchmark.py", line 171, in benchexec.benchexec.main(Benchmark())...

Draft: Prepare Release 6.0.0

3

To prepare the release of 6.0.0 we should discuss all changes that we included and want to include, as well as update our README and info material to reflect the...

JavaSMT is lacking a common API for proofs of unsatisfiablity. This is partially due to basically no two solvers using the same proof format. @gcarpio21 already worked quite a lot...

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

14

MathSAT5 throws a `NoSuchElementException` in the model in the following CPAchecker run `--symbolicExecution --stats --spec test/programs/benchmarks/properties/unreach-call.prp --32 --no-output-files test/programs/benchmarks/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-25_file-4.i` in this [branch/MR](https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/255) latest state. This looks like a bug, either...

Re-enable Z3 4.5.0 for better interpolation (continuation of #536)

7

This PR continues the work from [PR536](https://github.com/sosy-lab/java-smt/pull/536) with support from our CI etc. Original PR description from @leventeBajczi: Old versions of z3 were really good at interpolation, and I want...

Add CVC5 Parsing Support

5

This PR adds support for parsing to CVC5. Should only be merged after [PR539](https://github.com/sosy-lab/java-smt/pull/539).

Add IEEE-754 Floating Point to Bitvector Conversion Fallback

4

This PR adds 2 fallback methods for `FloatingPointManager.toIeeeBitvector(FloatingPointFormula)`: - `FloatingPointManager.toIeeeBitvector(FloatingPointFormula, String)`, returning the BV representation as a new variable with the given name. Special FP numbers are returned as the...

Bitwuzla Parsing Symbols Twice With Error

2

Bitwuzla parses a symbol twice and throws an error when parsing the following SMTLIB2 queries in order: ``` (declare-const |main::b@3| (_ BitVec 32)) (declare-const |main::a@4| (_ BitVec 32)) (declare-const |main::c@2|...

Fix Floating-Point Mantissa Not Including Sign Bit

23

While implementing [PR 512](https://github.com/sosy-lab/java-smt/pull/512) i found a problem in our implementation of FloatingPointType and number. Our returned significant precision is off by one, see [SMTLib2 standard page for Floating-Points](https://smt-lib.org/theories-FloatingPoint.shtml). E.g....

Multi-Dimensional array solving and/or model generation is broken for several solvers. For Princess this is already known and a issue exists here: #520. See tests added [here](https://github.com/sosy-lab/java-smt/commit/55e572eb16dbb1bcb48704ce14c24c78a976efa9). We should fix...