with

The with statement allows you to choose one more invariants.

Scope

A with statement is used with check / enumeration command.

Semantics

Choose one ore more invariants to be checked by Cyclone. If more than one invariants are chosen, Cyclone will find any counter-examples that will break at least one of the chosen invariants. If the with statement is not used, all well-defined invariants are chosen.

An Example

      check for  5 with (inv1,inv2,inv3)

Invariants inv1, inv2 and inv3 are chosen to be checked. Cyclone will returns a counter-example that can break any one of the three invariants, if there is any.

< Back