SV-COMP 22 Qualification Run Submission

This release contains the binaries and the source tree of the version which is submitted to the qualification run of the SV-COMP 2022 competition.

Minimal necessary packages for Ubuntu 20.04 LTS:

• openjdk-11-jre-headless
• libgomp1
• libmpfr-dev

Note: this release might contain unstable features and is NOT built from master.

v3.0.0

This release introduces alpha support for generic SMT-LIB compatible SMT solvers. Currently supported solvers are: Z3, MathSAT, CVC4, Yices2, Princess, SMTInterpol and Boolector. The support also includes interpolation support. For more information see the project page.

The release introduces theta-solver-smtlib-cli.jar that is a CLI to manage the different versions of solvers installed (see). The new solvers are only available on Linux and for the CFA frontend right now. The new solvers can be used by configuring the --solver, --abstraction-solver or --refinement-solver option of the theta-cfa-cli.jar tool (see).

v2.23.0

This release adds If statements to the XSTS language.

v2.22.3

This release fixes a bug in XSTS trace serialization

v2.22.2

This release includes a rework of the XSTS type system and some bugfixes

v2.22.1

This release adds some speed improvements to trace creation in the ARG. Thanks @asztrikx

v2.22.0

This release introduces ArrayInitExprs (see release v2.21.0) in the XSTS formalism.

v2.21.0

This release fixed the ArrayLitExpr expression, and introduces a new ArrayInitExpr expression.

Until this release, arbitrary expressions could be passed to ArrayLitExpr, which only handled LitExpr correctly (e.g. the simplification assumed that only evaluatable expressions are present). This release forbids non-fully-evaluatable expressions in ArrayLitExprs, but introduces ArrayInitExpr which fills the gap by providing support for arbitrary expressions. The grammar does not change, but every initialization expression is compiled into an ArrayInitExpr, which when simplifiable, gets transformed into an ArrayLitExpr.

v2.20.0

This release brings BigFloat support for the Win64 platform, enabling the use of the floating point type in Theta.
Note the occasional instability of the windows version, detailed in the CFA readme.

v2.19.0

Floating point types were introduced in v2.18.0, but the MPFR is only available on Linux (currently) so the Windows builds got broken. This release disables float tests on Windows to make the build possible, but of course floats will not be available. Some notes were added to readmes on this.

This release also adds array write syntactic sugar to the XSTS formalism: a[i] := v, which is equivalent to a := a[i <- v].