[SAL-HELP] Suspicious results

[David Friggens]

> In the attached file, I can't figure out why I would get a
> counter-example with F=201.

  main: MODULE =
    BEGIN
       OUTPUT F : INTEGER
    END;

This module doesn't have an INITIALIZATION section, so F can be 
initialized to any integer. Presumably you'll either need to give an 
initial value or define it (using DEFINITION) in terms of the other 
variables.

Cheers
David