## Revision 43a2cae9

View differences:

bench/distrib/misc/_6counter/_6counter.lus
1
```-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
```
2
```-- property is that it should never reach 6 or 7
```
3

4
```--@ ensures OK;
```
5
```node top (x:bool) returns (OK:bool);
```
6
```var a,b,c:bool;
```
7
```let
```
8
```  a = false -> not pre(a);
```
9
```  b = false -> (not pre(c) and not pre(b) and pre(a)) or
```
10
```           (pre(b) and not pre(a));
```
11
```  c = false -> (pre(c) and not pre(a)) or (pre(b) and pre(a));
```
12
```  OK = true -> pre(true -> pre b) = not b;
```
13
```--  --%PROPERTY not (c and b);
```
14
```--%PROPERTY OK;
```
15
```tel
```
bench/distrib/misc/_6counter/_6counter.lus_top_flatten.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/conds/_6counter.conds
1
```pre V6_c and (V5_b != (false -> ((((not pre (not V6_c)) and (not pre V5_b)) and pre V4_a) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
2
```(not pre V6_c) and (V5_b != (false -> ((((not pre (not V6_c)) and (not pre V5_b)) and pre V4_a) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
3
```pre V5_b and (V5_b != (false -> ((((not pre V6_c) and (not pre (not V5_b))) and pre V4_a) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
4
```(not pre V5_b) and (V5_b != (false -> ((((not pre V6_c) and (not pre (not V5_b))) and pre V4_a) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
5
```pre V4_a and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre (not V4_a)) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
6
```(not pre V4_a) and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre (not V4_a)) or (pre V5_b and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
7
```pre V5_b and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre V4_a) or (pre (not V5_b) and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
8
```(not pre V5_b) and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre V4_a) or (pre (not V5_b) and (not pre V4_a))))) and (x or not x) and (OK or not OK)
```
9
```pre V4_a and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre V4_a) or (pre V5_b and (not pre (not V4_a)))))) and (x or not x) and (OK or not OK)
```
10
```(not pre V4_a) and (V5_b != (false -> ((((not pre V6_c) and (not pre V5_b)) and pre V4_a) or (pre V5_b and (not pre (not V4_a)))))) and (x or not x) and (OK or not OK)
```
11
```pre V6_c and (V6_c != (false -> ((pre (not V6_c) and (not pre V4_a)) or (pre V5_b and pre V4_a)))) and (x or not x) and (OK or not OK)
```
12
```(not pre V6_c) and (V6_c != (false -> ((pre (not V6_c) and (not pre V4_a)) or (pre V5_b and pre V4_a)))) and (x or not x) and (OK or not OK)
```
13
```pre V4_a and (V6_c != (false -> ((pre V6_c and (not pre (not V4_a))) or (pre V5_b and pre V4_a)))) and (x or not x) and (OK or not OK)
```
14
```(not pre V4_a) and (V6_c != (false -> ((pre V6_c and (not pre (not V4_a))) or (pre V5_b and pre V4_a)))) and (x or not x) and (OK or not OK)
```
15
```pre V5_b and (V6_c != (false -> ((pre V6_c and (not pre V4_a)) or (pre (not V5_b) and pre V4_a)))) and (x or not x) and (OK or not OK)
```
16
```(not pre V5_b) and (V6_c != (false -> ((pre V6_c and (not pre V4_a)) or (pre (not V5_b) and pre V4_a)))) and (x or not x) and (OK or not OK)
```
17
```pre V4_a and (V6_c != (false -> ((pre V6_c and (not pre V4_a)) or (pre V5_b and pre (not V4_a))))) and (x or not x) and (OK or not OK)
```
18
```(not pre V4_a) and (V6_c != (false -> ((pre V6_c and (not pre V4_a)) or (pre V5_b and pre (not V4_a))))) and (x or not x) and (OK or not OK)
```
bench/distrib/misc/_6counter/conds/_6counter.ec
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n1.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n10.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n100.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n101.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) xor (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n102.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (not (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and
```
17
```  (pre V4_a)))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n103.lus
1
```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 = (true -> ((pre (true -> (pre (not V5_b)))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n104.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n105.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n106.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a))
```
15
```  and ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n107.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre (pre V6_c))) and (not (pre V5_b))) and (pre
```
15
```  V4_a)) or ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n108.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n109.lus
1
```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 = (true -> ((pre (not (true -> (pre V5_b)))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n11.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (not (pre V4_a))));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n110.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> (((not ((not (pre V6_c)) and (not (pre V5_b)))) and (pre
```
15
```  V4_a)) or ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n111.lus
1
```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 = (true -> ((not (pre (true -> (pre V5_b)))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n112.lus
1
```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 = (true -> ((pre (true -> (not (pre V5_b)))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n113.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre (pre V4_a
```
15
```  ))) or ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n114.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n115.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  (not ((pre V5_b) and (not (pre V4_a))))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n116.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or (not ((pre V5_b) and
```
17
```  (pre V4_a)))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n117.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre (pre V4_a))))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n118.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n119.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre (pre V4_a)))) or ((pre V5_b) and
```
17
```  (pre V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n12.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (not (pre V4_a))));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n120.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n121.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((not (pre V5_b)) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n122.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) >= (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n123.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n124.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre (pre V5_b)))) and (pre
```
15
```  V4_a)) or ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n125.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n126.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n127.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n128.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n129.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (not (pre V4_a))))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n13.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n130.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n131.lus
1
```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 = (true -> ((pre (pre (true -> (pre V5_b)))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n132.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) > (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n133.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n134.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n135.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n136.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (not
```
17
```  (pre V4_a)))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n137.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre (pre V6_c)) and (not (pre V4_a))) or ((pre V5_b) and
```
17
```  (pre V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n138.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n139.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) or (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n14.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n140.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n141.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre (not V5_b)))) and (pre
```
15
```  V4_a)) or ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n142.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre (not V5_b)) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n143.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre (pre V5_b)) and
```
17
```  (pre V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n144.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n145.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (not (pre V4_a)))) or ((pre V5_b) and
```
17
```  (pre V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n146.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n147.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n148.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) <= (not V5_b)));
```
13
```  V4_a = (false -> (not (pre V4_a)));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

bench/distrib/misc/_6counter/mutants/_6counter.mutant.n149.lus
1
```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 = (true -> ((pre (true -> (pre V5_b))) = (not V5_b)));
```
13
```  V4_a = (false -> (not (pre (pre V4_a))));
```
14
```  V5_b = (false -> ((((not (pre V6_c)) and (not (pre V5_b))) and (pre V4_a)) or
```
15
```  ((pre V5_b) and (not (pre V4_a)))));
```
16
```  V6_c = (false -> (((pre V6_c) and (not (pre V4_a))) or ((pre V5_b) and (pre
```
17
```  V4_a))));
```
18
```tel
```
19

... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff