1. Running test 0: 6 × 7 using a loop.
2. Running test 1: an assignment.
3. Running test 2: limitation of the absence of meet after branching.
4. Running test 3: a loop for which the signs does not fit.
5. Running test 4: an unexecuted loop.
6. Running test 5: a neverending loop.
7. Running test 6: a relatively long computation without loop.
8. Running test 7: a loop terminating after two unfoldings.
9. Running test 8: a loop terminating after four unfoldings.
10. Running test 9: testing [if] and [throw].
11. Running test 10: a loop terminating after four unfoldings with tests.
12. Running test 11: nested loops.
13. Running test 12: a loop whose termination is difficult to tell.

Running the analysers on different tests.

1 Running test 0: 6 × 7 using a loop.

1.1 Program

[ a := (6) ;
  b := (7) ;
  n := (a) ;
  res := (0) ;
  while (n)
  do res := ((res) + (b)) ;
     n := ((n) + (-1))
  od ]

On context: { _ -> Undef }.

1.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

1.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

1.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

1.4.1 Failed at

[ (7) ]
On context:
{ a -> +, _ -> Undef }.

1.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

1.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

Failed to get a result.

1.6.1 Failed at

[ (-1) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.

1.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

1.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

1.8.1 Failed at

[ while1 (n)
  do res := ((res) + (b)) ;
     n := ((n) + (-1))
  od ]
On context:
while1 (stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).

1.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

1.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

Failed to get a result.

1.10.1 Failed at

[ while1 (n)
  do res := ((res) + (b)) ;
     n := ((n) + (-1))
  od ]
On context:
while1 (stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).

1.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

1.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

1.12.1 Failed at

[ ((n) + (-1)) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef }.

1.12.2 Oracle hint

[ (res) ]
On context:
{ res -> 0, n -> +, b -> +, a -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

1.12.3 Oracle hint

[ add1 (b) ]
On context:
add1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
expr (+ , <no error>).

1.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

Failed to get a result.

1.13.1 Failed at

[ (res) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.

1.13.2 Oracle hint

[ (-1) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

1.13.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

1.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

1.14.1 Failed at

[ ((n) + (-1)) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef }.

1.14.2 Oracle hint

[ (res) ]
On context:
{ res -> 0, n -> +, b -> +, a -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

1.14.3 Oracle hint

[ add1 (b) ]
On context:
add1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
expr (+ , <no error>).

1.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

Failed to get a result.

1.15.1 Failed at

[ (res) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.

1.15.2 Oracle hint

[ (-1) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

1.15.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

1.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

1.20.1 Failed at

[ ((n) + (-1)) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef }.

1.20.2 Oracle hint

[ (res) ]
On context:
{ res -> 0, n -> +, b -> +, a -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

1.20.3 Oracle hint

[ add1 (b) ]
On context:
add1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
expr (+ , <no error>).

1.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

Failed to get a result.

1.21.1 Failed at

[ (res) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.

1.21.2 Oracle hint

[ (-1) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

1.21.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

1.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

1.22.1 Failed at

[ ((n) + (-1)) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef }.

1.22.2 Oracle hint

[ (res) ]
On context:
{ res -> 0, n -> +, b -> +, a -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

1.22.3 Oracle hint

[ add1 (b) ]
On context:
add1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
expr (+ , <no error>).

1.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

Failed to get a result.

1.23.1 Failed at

[ (res) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.

1.23.2 Oracle hint

[ (-1) ]
On context:
{ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

1.23.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

1.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

1.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ res -> +, n -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)

2 Running test 1: an assignment.

2.1 Program

[ x := (42) ]

On context: { _ -> Undef }.

2.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

2.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

2.4 Running analyser: `sign_analyse_fuel_fail 4`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

2.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

3 Running test 2: limitation of the absence of meet after branching.

3.1 Program

[ if ((x) + (1))
   then y := (-1)
   else y := (x)
  fi ]

On context: { x -> Top (sign), _ -> Undef }.

3.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

3.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

3.4 Running analyser: `sign_analyse_fuel_fail 4`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

3.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef } , <no error>)

4 Running test 3: a loop for which the signs does not fit.

4.1 Program

[ while (x)
  do x := ((x) + (1))
  od ]

On context: { x -> Top (sign), _ -> Undef }.

4.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

4.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

4.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

4.4.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

4.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

Failed to get a result.

4.6.1 Failed at

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

4.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

4.8.1 Failed at

[ while1 (x)
  do x := ((x) + (1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), _ -> Undef } , <no error>)).

4.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

4.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

Failed to get a result.

4.10.1 Failed at

[ while1 (x)
  do x := ((x) + (1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), _ -> Undef } , <no error>)).

4.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

4.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

4.12.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.12.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.12.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

Failed to get a result.

4.13.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.13.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.13.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

4.14.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.14.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.14.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

Failed to get a result.

4.15.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.15.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.15.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

4.20.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.20.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.20.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

Failed to get a result.

4.21.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.21.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.21.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

4.22.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.22.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.22.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

Failed to get a result.

4.23.1 Failed at

[ ((x) + (1)) ]
On context:
{ x -> Top (sign), _ -> Undef }.

4.23.2 Oracle hint

[ (1) ]
On context:
{ x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

4.23.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (+ , <no error>)).
With result:
expr (Top (sign) , <no error>).

4.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

4.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5 Running test 4: an unexecuted loop.

5.1 Program

[ while (0)
  do x := (42)
  od ]

On context: { x -> Top (sign), _ -> Undef }.

5.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

5.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

5.4 Running analyser: `sign_analyse_fuel_fail 4`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

5.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <no error>)

6 Running test 5: a neverending loop.

6.1 Program

[ while (1)
  do x := (42)
  od ]

On context: { x -> Top (sign), _ -> Undef }.

6.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

6.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

6.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

6.4.1 Failed at

[ (42) ]
On context:
{ x -> Top (sign), _ -> Undef }.

6.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

6.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

Failed to get a result.

6.6.1 Failed at

[ (42) ]
On context:
{ x -> +, _ -> Undef }.

6.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

6.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

6.8.1 Failed at

[ while1 (1)
  do x := (42)
  od ]
On context:
while1 (stat ({ x -> +, _ -> Undef } , <no error>)).

6.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

6.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

Failed to get a result.

6.10.1 Failed at

[ while1 (1)
  do x := (42)
  od ]
On context:
while1 (stat ({ x -> +, _ -> Undef } , <no error>)).

6.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

6.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

6.12.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.12.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.12.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

Failed to get a result.

6.13.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.13.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.13.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

6.14.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.14.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.14.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

Failed to get a result.

6.15.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.15.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.15.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: Bot

6.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: Bot

6.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: Bot

6.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: Bot

6.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

6.20.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.20.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.20.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

Failed to get a result.

6.21.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.21.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.21.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

6.22.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.22.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.22.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

Failed to get a result.

6.23.1 Failed at

[ (1) ]
On context:
{ x -> +, _ -> Undef }.

6.23.2 Oracle hint

[ (42) ]
On context:
{ x -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

6.23.3 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> +, _ -> Undef } , <no error>).

6.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: Bot

6.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: Bot

6.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: Bot

6.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: Bot

6.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: Bot

6.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: Bot

6.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: Bot

6.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: Bot

6.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: Bot

6.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: Bot

6.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: Bot

6.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: Bot

6.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: Bot

6.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: Bot

6.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: Bot

6.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: Bot

6.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: Bot

6.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: Bot

6.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: Bot

6.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: Bot

7 Running test 6: a relatively long computation without loop.

7.1 Program

[ x := ((42) + ((18) + (17))) ]

On context: { _ -> Undef }.

7.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

7.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

7.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

7.4.1 Failed at

[ (18) ]
On context:
{ _ -> Undef }.

7.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ x -> Top (sign), _ -> Undef } , <may be an error>)

7.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

7.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> +, _ -> Undef } , <no error>)

8 Running test 7: a loop terminating after two unfoldings.

8.1 Program

[ x := (1) ;
  while (x)
  do x := (0)
  od ]

On context: { _ -> Undef }.

8.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

8.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

8.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

8.4.1 Failed at

[ (x) ]
On context:
{ x -> +, _ -> Undef }.

8.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

8.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

8.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> 0, _ -> Undef } , <no error>)

9 Running test 8: a loop terminating after four unfoldings.

9.1 Program

[ x := (1) ;
  y := (1) ;
  z := (1) ;
  while (x)
  do x := (y) ;
     y := (z) ;
     z := (0)
  od ]

On context: { _ -> Undef }.

9.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

9.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

9.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

9.4.1 Failed at

[ y := (1) ]
On context:
{ x -> +, _ -> Undef }.

9.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

9.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

9.8.1 Failed at

[ while1 (x)
  do x := (y) ;
     y := (z) ;
     z := (0)
  od ]
On context:
while1 (stat ({ z -> 0, y -> 0, x -> +, _ -> Undef } , <no error>)).

9.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

9.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

9.12.1 Failed at

[ y := (z) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.

9.12.2 Oracle hint

[ (0) ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

9.12.3 Oracle hint

[ z (:=)1 ]
On context:
asgn1 ({ z -> +, y -> +, x -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
stat ({ z -> 0, y -> +, x -> +, _ -> Undef } , <no error>).

9.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

9.14.1 Failed at

[ y := (z) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.

9.14.2 Oracle hint

[ (0) ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

9.14.3 Oracle hint

[ z (:=)1 ]
On context:
asgn1 ({ z -> +, y -> +, x -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
stat ({ z -> 0, y -> +, x -> +, _ -> Undef } , <no error>).

9.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

9.20.1 Failed at

[ y := (z) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.

9.20.2 Oracle hint

[ (0) ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

9.20.3 Oracle hint

[ z (:=)1 ]
On context:
asgn1 ({ z -> +, y -> +, x -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
stat ({ z -> 0, y -> +, x -> +, _ -> Undef } , <no error>).

9.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

9.22.1 Failed at

[ y := (z) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.

9.22.2 Oracle hint

[ (0) ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

9.22.3 Oracle hint

[ z (:=)1 ]
On context:
asgn1 ({ z -> +, y -> +, x -> +, _ -> Undef } , expr (0 , <no error>)).
With result:
stat ({ z -> 0, y -> +, x -> +, _ -> Undef } , <no error>).

9.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

9.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

10 Running test 9: testing [if] and [throw].

10.1 Program

[ if (x)
   then throw
   else skip
  fi ]

On context: { _ -> Undef }.

10.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

10.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

10.4 Running analyser: `sign_analyse_fuel_fail 4`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

10.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ _ -> Bot } , <may be an error>)

11 Running test 10: a loop terminating after four unfoldings with tests.

11.1 Program

[ x := (1) ;
  y := (1) ;
  z := (1) ;
  while (z)
  do if (y)
      then z := (0)
      else skip
     fi ;
     if (x)
      then y := (0)
      else skip
     fi ;
     x := (0)
  od ]

On context: { _ -> Undef }.

11.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

11.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

11.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

11.4.1 Failed at

[ y := (1) ]
On context:
{ x -> +, _ -> Undef }.

11.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

11.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

11.12.1 Failed at

[ x (:=)1 ]
On context:
asgn1 ({ z -> 0, y -> 0, x -> +, _ -> Undef } , expr (0 , <no error>)).

11.12.2 Oracle hint

[ (0) ]
On context:
{ z -> 0, y -> 0, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

11.12.3 Oracle hint

[ y := (0) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.
With result:
stat ({ z -> 0, y -> 0, x -> +, _ -> Undef } , <no error>).

11.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

11.14.1 Failed at

[ x (:=)1 ]
On context:
asgn1 ({ z -> 0, y -> 0, x -> +, _ -> Undef } , expr (0 , <no error>)).

11.14.2 Oracle hint

[ (0) ]
On context:
{ z -> 0, y -> 0, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

11.14.3 Oracle hint

[ y := (0) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.
With result:
stat ({ z -> 0, y -> 0, x -> +, _ -> Undef } , <no error>).

11.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

11.20.1 Failed at

[ x (:=)1 ]
On context:
asgn1 ({ z -> 0, y -> 0, x -> +, _ -> Undef } , expr (0 , <no error>)).

11.20.2 Oracle hint

[ (0) ]
On context:
{ z -> 0, y -> 0, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

11.20.3 Oracle hint

[ y := (0) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.
With result:
stat ({ z -> 0, y -> 0, x -> +, _ -> Undef } , <no error>).

11.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

11.22.1 Failed at

[ x (:=)1 ]
On context:
asgn1 ({ z -> 0, y -> 0, x -> +, _ -> Undef } , expr (0 , <no error>)).

11.22.2 Oracle hint

[ (0) ]
On context:
{ z -> 0, y -> 0, x -> +, _ -> Undef }.
With result:
expr (0 , <no error>).

11.22.3 Oracle hint

[ y := (0) ]
On context:
{ z -> 0, y -> +, x -> +, _ -> Undef }.
With result:
stat ({ z -> 0, y -> 0, x -> +, _ -> Undef } , <no error>).

11.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

11.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef } , <no error>)

12 Running test 11: nested loops.

12.1 Program

[ a := (5) ;
  while (a)
  do b := (5) ;
     while (b)
     do c := (5) ;
        while (c)
        do x := ((x) + (c)) ;
           c := ((c) + (-1))
        od ;
        b := ((b) + (-1))
     od ;
     a := ((a) + (-1))
  od ]

On context: { x -> Top (sign), _ -> Undef }.

12.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

12.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

12.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

12.4.1 Failed at

[ (a) ]
On context:
{ x -> Top (sign), a -> +, _ -> Undef }.

12.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

12.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

Failed to get a result.

12.6.1 Failed at

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.

12.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

12.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

12.8.1 Failed at

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).

12.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

12.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

Failed to get a result.

12.10.1 Failed at

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).

12.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

12.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

12.12.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.12.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.12.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

Failed to get a result.

12.13.1 Failed at

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.

12.13.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.13.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

12.14.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.14.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.14.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

Failed to get a result.

12.15.1 Failed at

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.

12.15.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.15.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Failure)

Failed to get a result.

12.16.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.16.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.16.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Failure)

Failed to get a result.

12.17.1 Failed at

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }.

12.17.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.17.3 Oracle hint

[ (c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.17.4 Oracle hint

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.17.5 Oracle hint

[ ((c) + (-1)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.17.6 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.17.7 Oracle hint

[ add1 (c) ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.17.8 Oracle hint

[ x := ((x) + (c)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.17.9 Oracle hint

[ c (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.17.10 Oracle hint

[ (;)1
  c := ((c) + (-1)) ]
On context:
seq1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.17.11 Oracle hint

[ while2 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Failure)

Failed to get a result.

12.18.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.18.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.18.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Failure)

Failed to get a result.

12.19.1 Failed at

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }.

12.19.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.19.3 Oracle hint

[ (c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.19.4 Oracle hint

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.19.5 Oracle hint

[ ((c) + (-1)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.19.6 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.19.7 Oracle hint

[ add1 (c) ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.19.8 Oracle hint

[ x := ((x) + (c)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.19.9 Oracle hint

[ c (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.19.10 Oracle hint

[ (;)1
  c := ((c) + (-1)) ]
On context:
seq1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.19.11 Oracle hint

[ while2 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

12.20.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.20.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.20.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

Failed to get a result.

12.21.1 Failed at

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.

12.21.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.21.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

12.22.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.22.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.22.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

Failed to get a result.

12.23.1 Failed at

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.

12.23.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.23.3 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Failure)

Failed to get a result.

12.24.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.24.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.24.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Failure)

Failed to get a result.

12.25.1 Failed at

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }.

12.25.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.25.3 Oracle hint

[ (c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.25.4 Oracle hint

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.25.5 Oracle hint

[ ((c) + (-1)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.25.6 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.25.7 Oracle hint

[ add1 (c) ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.25.8 Oracle hint

[ x := ((x) + (c)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.25.9 Oracle hint

[ c (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.25.10 Oracle hint

[ (;)1
  c := ((c) + (-1)) ]
On context:
seq1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.25.11 Oracle hint

[ while2 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Failure)

Failed to get a result.

12.26.1 Failed at

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).

12.26.2 Oracle hint

[ (b) ]
On context:
{ x -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (+ , <no error>).

12.26.3 Oracle hint

[ while2 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (+ , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Failure)

Failed to get a result.

12.27.1 Failed at

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }.

12.27.2 Oracle hint

[ (-1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (- , <no error>).

12.27.3 Oracle hint

[ (c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.27.4 Oracle hint

[ (x) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.27.5 Oracle hint

[ ((c) + (-1)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
expr (Top (sign) , <no error>).

12.27.6 Oracle hint

[ add2 ]
On context:
add2 (Top (sign) , expr (- , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.27.7 Oracle hint

[ add1 (c) ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
expr (Top (sign) , <no error>).

12.27.8 Oracle hint

[ x := ((x) + (c)) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }.
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.27.9 Oracle hint

[ c (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.27.10 Oracle hint

[ (;)1
  c := ((c) + (-1)) ]
On context:
seq1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.27.11 Oracle hint

[ while2 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while2 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , expr (Top (sign) , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Failure)

Failed to get a result.

12.28.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.28.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.28.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Failure)

Failed to get a result.

12.29.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.29.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.29.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Failure)

Failed to get a result.

12.30.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.30.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.30.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Failure)

Failed to get a result.

12.31.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.31.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.31.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Failure)

Failed to get a result.

12.32.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.32.2 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).

12.32.3 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.32.4 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>).

12.32.5 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.32.6 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.32.7 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>).

12.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)

12.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Failure)

Failed to get a result.

12.34.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.34.2 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).

12.34.3 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.34.4 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>).

12.34.5 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.34.6 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.34.7 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>).

12.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)

12.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Failure)

Failed to get a result.

12.36.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.36.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.36.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Failure)

Failed to get a result.

12.37.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.37.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.37.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Failure)

Failed to get a result.

12.38.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.38.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.38.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Failure)

Failed to get a result.

12.39.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.39.2 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.39.3 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Failure)

Failed to get a result.

12.40.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.40.2 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).

12.40.3 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.40.4 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>).

12.40.5 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.40.6 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.40.7 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>).

12.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)

12.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Failure)

Failed to get a result.

12.42.1 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).

12.42.2 Failed at

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).

12.42.3 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.42.4 Oracle hint

[ while1 (b)
  do c := (5) ;
     while (c)
     do x := ((x) + (c)) ;
        c := ((c) + (-1))
     od ;
     b := ((b) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>).

12.42.5 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } , <no error>).

12.42.6 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } , <no error>).

12.42.7 Oracle hint

[ while1 (c)
  do x := ((x) + (c)) ;
     c := ((c) + (-1))
  od ]
On context:
while1 (stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> Top (sign), _ -> Undef } , <no error>).

12.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef } , <no error>)

13 Running test 12: a loop whose termination is difficult to tell.

13.1 Program

[ y := (0) ;
  x := (18) ;
  while (x)
  do x := ((x) + (-1)) ;
     y := ((y) + (1))
  od ]

On context: { _ -> Undef }.

13.2 Running analyser: `sign_trivial_analyser`. (Success)

Terminated with result: Top

13.3 Running analyser: `sign_type_analyse`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

13.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

Failed to get a result.

13.4.1 Failed at

[ (18) ]
On context:
{ y -> 0, _ -> Undef }.

13.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

13.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

Failed to get a result.

13.6.1 Failed at

[ (1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

13.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

Failed to get a result.

13.8.1 Failed at

[ while1 (x)
  do x := ((x) + (-1)) ;
     y := ((y) + (1))
  od ]
On context:
while1 (stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)).

13.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

13.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

Failed to get a result.

13.10.1 Failed at

[ while1 (x)
  do x := ((x) + (-1)) ;
     y := ((y) + (1))
  od ]
On context:
while1 (stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)).

13.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

Terminated with result: stat ({ _ -> Top (valvar) } , <may be an error>)

13.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

Failed to get a result.

13.12.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.12.2 Oracle hint

[ (1) ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.12.3 Oracle hint

[ add2 ]
On context:
add2 (0 , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

Failed to get a result.

13.13.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.13.2 Oracle hint

[ (1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.13.3 Oracle hint

[ add2 ]
On context:
add2 (+ , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

Failed to get a result.

13.14.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.14.2 Oracle hint

[ (1) ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.14.3 Oracle hint

[ add2 ]
On context:
add2 (0 , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

Failed to get a result.

13.15.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.15.2 Oracle hint

[ (1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.15.3 Oracle hint

[ add2 ]
On context:
add2 (+ , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

Failed to get a result.

13.20.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.20.2 Oracle hint

[ (1) ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.20.3 Oracle hint

[ add2 ]
On context:
add2 (0 , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

Failed to get a result.

13.21.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.21.2 Oracle hint

[ (1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.21.3 Oracle hint

[ add2 ]
On context:
add2 (+ , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

Failed to get a result.

13.22.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.22.2 Oracle hint

[ (1) ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.22.3 Oracle hint

[ add2 ]
On context:
add2 (0 , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

Failed to get a result.

13.23.1 Failed at

[ (x) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.

13.23.2 Oracle hint

[ (1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef }.
With result:
expr (+ , <no error>).

13.23.3 Oracle hint

[ add2 ]
On context:
add2 (+ , expr (+ , <no error>)).
With result:
expr (+ , <no error>).

13.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

13.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

Terminated with result: stat ({ y -> +, x -> Top (sign), _ -> Undef } , <no error>)

Table of Contents

1 Running test 0: 6 × 7 using a loop.

1.1 Program

1.2 Running analyser: sign_trivial_analyser. (Success)

1.3 Running analyser: sign_type_analyse. (Success)

1.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

1.4.1 Failed at

1.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

1.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

1.6.1 Failed at

1.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

1.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

1.8.1 Failed at

1.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

1.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

1.10.1 Failed at

1.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

1.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

1.12.1 Failed at

1.12.2 Oracle hint

1.12.3 Oracle hint

1.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Failure)

1.13.1 Failed at

1.13.2 Oracle hint

1.13.3 Oracle hint

1.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

1.14.1 Failed at

1.14.2 Oracle hint

1.14.3 Oracle hint

1.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Failure)

1.15.1 Failed at

1.15.2 Oracle hint

1.15.3 Oracle hint

1.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

1.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

1.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

1.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

1.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

1.20.1 Failed at

1.20.2 Oracle hint

1.20.3 Oracle hint

1.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Failure)

1.21.1 Failed at

1.21.2 Oracle hint

1.21.3 Oracle hint

1.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

1.22.1 Failed at

1.22.2 Oracle hint

1.22.3 Oracle hint

1.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Failure)

1.23.1 Failed at

1.23.2 Oracle hint

1.23.3 Oracle hint

1.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

1.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

1.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

1.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

1.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

1.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

1.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

1.31 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 3 2. (Success)

1.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

1.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

1.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

1.35 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 3 10. (Success)

1.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Success)

1.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

1.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Success)

1.39 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2. (Success)

1.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Success)

1.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

1.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Success)

1.43 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10. (Success)

2 Running test 1: an assignment.

2.1 Program

2.2 Running analyser: sign_trivial_analyser. (Success)

2.3 Running analyser: sign_type_analyse. (Success)

2.4 Running analyser: sign_analyse_fuel_fail 4. (Success)

2.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

2.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

1.2 Running analyser: `sign_trivial_analyser`. (Success)

1.3 Running analyser: `sign_type_analyse`. (Success)

1.4 Running analyser: `sign_analyse_fuel_fail 4`. (Failure)

1.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

1.6 Running analyser: `sign_analyse_fuel_fail 100`. (Failure)

1.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

1.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Failure)

1.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

1.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Failure)

1.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

1.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Failure)

1.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Failure)

1.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Failure)

1.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Failure)

1.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

1.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

1.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

1.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

1.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Failure)

1.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Failure)

1.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Failure)

1.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Failure)

1.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

1.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

1.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

1.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

1.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

1.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

1.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

1.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

1.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

1.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

1.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

1.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

1.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

1.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

1.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

1.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)

1.40 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10`. (Success)

1.41 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10`. (Success)

1.42 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10`. (Success)

1.43 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10`. (Success)

2.2 Running analyser: `sign_trivial_analyser`. (Success)

2.3 Running analyser: `sign_type_analyse`. (Success)

2.4 Running analyser: `sign_analyse_fuel_fail 4`. (Success)

2.5 Running analyser: `sign_analyse_fuel type_analyse 4`. (Success)

2.6 Running analyser: `sign_analyse_fuel_fail 100`. (Success)

2.7 Running analyser: `sign_analyse_fuel type_analyse 100`. (Success)

2.8 Running analyser: `sign_analyse_deep_fuel_fail 1`. (Success)

2.9 Running analyser: `sign_analyse_deep_fuel type_analyse 1`. (Success)

2.10 Running analyser: `sign_analyse_deep_fuel_fail 10`. (Success)

2.11 Running analyser: `sign_analyse_deep_fuel type_analyse 10`. (Success)

2.12 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 2`. (Success)

2.13 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 2`. (Success)

2.14 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 2`. (Success)

2.15 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 2`. (Success)

2.16 Running analyser: `sign_analyse_oracle_back_and_forth 10 1 10`. (Success)

2.17 Running analyser: `sign_analyse_oracle_back_and_forth 50 1 10`. (Success)

2.18 Running analyser: `sign_analyse_oracle_back_and_forth 10 3 10`. (Success)

2.19 Running analyser: `sign_analyse_oracle_back_and_forth 50 3 10`. (Success)

2.20 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 2`. (Success)

2.21 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 2`. (Success)

2.22 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 2`. (Success)

2.23 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 2`. (Success)

2.24 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 1 10`. (Success)

2.25 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 1 10`. (Success)

2.26 Running analyser: `sign_analyse_oracle_back_and_forth_loop 10 3 10`. (Success)

2.27 Running analyser: `sign_analyse_oracle_back_and_forth_loop 50 3 10`. (Success)

2.28 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 2`. (Success)

2.29 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 2`. (Success)

2.30 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 2`. (Success)

2.31 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 2`. (Success)

2.32 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 1 10`. (Success)

2.33 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 1 10`. (Success)

2.34 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 1 3 10`. (Success)

2.35 Running analyser: `sign_analyse_oracle_back_and_forth_deep 1 5 3 10`. (Success)

2.36 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2`. (Success)

2.37 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2`. (Success)

2.38 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2`. (Success)

2.39 Running analyser: `sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2`. (Success)