This tag is the last tag before the horn solver and lazy SC solver are removed.

From a user perspective, this release contains some bug fixes and a new synthesis interface.
From a developer perspective, this tag marks a significant change in the git history.

This release
uclid-0.9.5.zip
contains a few more bugfixes.

Main new feature in this release is hyperproperty verification using BMC. See test/test-hyperproperty-*.ucl for examples.

We have also added support for quantifier patterns. See examples/hash.ucl for an example.

Several bugs have been fixed.

We have experimental support for unbounded model checking using the Z3/SPACER. Documentation for this feature will be added when this feature becomes more stable.

What's new?

• Much improved tutorial.
• Initial support for SyGuS
• New operators (distinct, bv_sign_extend, bv_zero_extend).
• Local scoped variables are allowed in every block now.
• We have the beginnings of an optimizer.
• Lots and lots and lots of bugfixes.

UCLID5 v0.9.1 Release

What's new?

• Support for mixing procedural and parallel modeling using primed variables.
• Simplified syntax by removing '::' and '->' operators and replacing them with '.'
• Support for constant literals and their use in for loops.
• Verifier bugfixes.

New to this release:

• Support for (bounded) model checking of LTL properties.
• Added the define keyword for defining macros.
• Performance improvements in the VC generator.
• Lots and lots of bugfixes.

uclid-0.8.zip