Version 0.5

This is the latest stable 0.5 release.

Changes since 0.4 include many bug fixes as well as improvements in the language and theorem prover back-end.

Language improvements:

• map comprehensions
• if-the-else expressions in definitions
• with clause for proving quantified assertions semi-manually

Back-end improvements:

• model REPL
• new E-matching engine
• more robust support for ADTs
• better support for quantifiers that do not fall into the decidable fragment

Version 0.4

This is the latest stable 0.4 release.

Changes since 0.3 include many bug fixes and several language improvements such as

• set comprehensions
• algebraic data types
• lemmas
• recursive predicates and functions
• macro definitions
• cleaner predicate/function syntax

Version 0.3.1

This is the latest stable 0.3 release.

Version 0.3

This version supports all the features described in our CAV'14 paper.