Revision 2d37a1e1 regression_tests/lustre_files/success/kind_fmcad08/misc/_6counters_e8_371_e1_448.lus
regression_tests/lustre_files/success/kind_fmcad08/misc/_6counters_e8_371_e1_448.lus | ||
---|---|---|
16 | 16 |
out = time = 5; |
17 | 17 |
tel |
18 | 18 |
|
19 |
--@ ensures OK; |
|
20 | 19 |
node top (x:bool) returns (OK:bool); |
20 |
--@ contract guarantees OK; |
|
21 | 21 |
var a,b:bool; |
22 | 22 |
let |
23 | 23 |
OK = a=b; |
Also available in: Unified diff