v2.16.0

This release adds automatic predicate-to-explicit switching strategies for product domains, and fixes havocs for enum variables.

v2.15.0

This release introduces the dedicated prod domain, EXPL_PRED_COMBINED.

v2.14.1

This release fixes a bug in XSTS parsing

v2.14.0

This release fixes the CI builds by changing the source of the Z3 dependency from bintray to a local jar.

v2.13.0

This release introduces a number of new features and improvements to the XSTS formalism:

• For loops (experimental)
• Statement optimization: the algorithm can significantly reduce the size of expressions passed to the solver by detecting unreachable branches of choice statements or failing assumptions
• The previous product domains were unified, and corresponding product domain variants were introduced for PRED_SPLIT and PRED_BOOL
• Dotfile visualization of counterexamples and the ARG
• Bugfixes

v2.12.1

This release adds a new expression for rational to int type conversion.

v2.12.0

This release improves XSTS local variables, which can now be declared more freely and can contain initial value assignments.

v2.11.1

This patch fixes a bug in counterexample serialization.

v2.11.0

This release adds support for local variables in the XSTS language.

v2.10.0

This release adds support for arrays in the XSTS formalism.