lustrec / bench / distrib / misc / stalmark_e7_27_e7_31 / mutants / stalmark_e7_27_e7_31.mutant.n79.lus @ 53aa0cb0
History | View | Annotate | Download (405 Bytes)
| 1 | 53aa0cb0 | ploc | node top |
|---|---|---|---|
| 2 | (x: bool) |
||
| 3 | returns |
||
| 4 | (OK: bool); |
||
| 5 | |||
| 6 | var |
||
| 7 | V4_a: bool; |
||
| 8 | V5_b: bool; |
||
| 9 | V6_c: bool; |
||
| 10 | |||
| 11 | let |
||
| 12 | OK = (((((((not V4_a) or (not V5_b)) or V6_c) or (((not V4_a) and V5_b) and |
||
| 13 | (not V6_c))) or ((V4_a and (not V5_b)) and (not V6_c))) or ((V4_a and V5_b) |
||
| 14 | and V6_c)) and (not ((V4_a and V5_b) and V6_c))); |
||
| 15 | V4_a = (true -> (pre V6_c)); |
||
| 16 | V5_b = (false -> (pre V4_a)); |
||
| 17 | V6_c = (false -> (pre V5_b)); |
||
| 18 | tel |