Project

General

Profile

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