Various checks for CIF checker crash for violations in the root of the specification
E.g., NoInitPredsInCompsCheck crashes if an initialization predicate is found in the root of the specification. That is because the component that contains that predicate is supplied as the named CIF object for the violations. However, a Specification
is not a named CIF object.
For example, try the following model with CIF to Supremica converter:
initial 1 = 1;
or
invariant 8 = 8;
Edited by Dennis Hendriks