0.4.0-pre1

0.4.0-pre1

• type annotations and very simple type inference, see the notes

• a dramatic speed up of many operators by using a QF_NIA theory and cherry pick

• automatic simplification of expressions, including equality

• decomposition of invariants into smaller pieces

Z3 and linux compatibility fix of version 0.2.0

This version fixes two issues that were introduced in version 0.2.0:

1. The script apalache-mc could not discover the distribution jar in linux (worked in macos)
2. By default, z3 4.8.0 was compiled, which introduced a new incompatible API. Now using version 4.7.1.

Version 0.2.0 presented at the TLA+ community event

This is the version of the tool that was presented at the TLA+ community meeting 2018. While it works on the presented examples, it may crash on your own code. This version is lacking support for sequences, recursive operators, set cardinalities, and module instantiation.

If you want to share your code that should be supported by BMCMT, feel free to submit a bug report or a feature request.