Table of Contents

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 } | <empty context>, <procedures defined: > (prog).

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

[ 6 ]
On context:
{ _ -> Undef } | <empty context> (expr).

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

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

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 (<empty context>, <procedures defined:  >, 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 (<empty context>, <procedures defined:  >, 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 := (n + -1) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

1.12.2 Oracle hint

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

1.12.3 Oracle hint

[ res (:=)1 ]
On context:
asgn1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, expr (+, <no error>)).
With result:
stat ({ res -> +, n -> +, b -> +, a -> +, _ -> Undef }, <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

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

1.13.2 Oracle hint

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

1.13.3 Oracle hint

[ add2 ]
On context:
add2 (+, expr (+, <no error>)).
With result:
expr (+, <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 := (n + -1) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

1.14.2 Oracle hint

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

1.14.3 Oracle hint

[ res (:=)1 ]
On context:
asgn1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, expr (+, <no error>)).
With result:
stat ({ res -> +, n -> +, b -> +, a -> +, _ -> Undef }, <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

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

1.15.2 Oracle hint

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

1.15.3 Oracle hint

[ add2 ]
On context:
add2 (+, expr (+, <no error>)).
With result:
expr (+, <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 := (n + -1) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

1.20.2 Oracle hint

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

1.20.3 Oracle hint

[ res (:=)1 ]
On context:
asgn1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, expr (+, <no error>)).
With result:
stat ({ res -> +, n -> +, b -> +, a -> +, _ -> Undef }, <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

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

1.21.2 Oracle hint

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

1.21.3 Oracle hint

[ add2 ]
On context:
add2 (+, expr (+, <no error>)).
With result:
expr (+, <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 := (n + -1) ]
On context:
{ res -> +, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

1.22.2 Oracle hint

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

1.22.3 Oracle hint

[ res (:=)1 ]
On context:
asgn1 ({ res -> 0, n -> +, b -> +, a -> +, _ -> Undef } | <empty context>, expr (+, <no error>)).
With result:
stat ({ res -> +, n -> +, b -> +, a -> +, _ -> Undef }, <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

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

1.23.2 Oracle hint

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

1.23.3 Oracle hint

[ add2 ]
On context:
add2 (+, expr (+, <no error>)).
With result:
expr (+, <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 } | <empty context>, <procedures defined: > (prog).

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 } | <empty context>, <procedures defined: > (prog).

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. (Failure)

Failed to get a result.

3.4.1 Failed at

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

3.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

Terminated with result: stat ({ _ -> Top (valvar) }, <may be an 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: simpler variation of the previous example.

4.1 Program

[ if x
   then y := 0
   else y := x
  fi ; ]

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

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

[ 0 ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context> (expr).

4.4.2 Failed at

[ x ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context> (expr).

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. (Success)

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

4.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

4.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

4.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

4.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

4.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

4.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>)

5 Running test 4: variation of the previous example.

5.1 Program

[ if x
   then x := 0
   else skip
  fi ; ]

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

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. (Failure)

Failed to get a result.

5.4.1 Failed at

[ 0 ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context> (expr).

5.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

Terminated with result: stat ({ _ -> Top (valvar) }, <may be an 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 loop for which the signs does not fit.

6.1 Program

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

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

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

[ x ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context> (expr).

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 x
  do x := (x + 1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), _ -> 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 x
  do x := (x + 1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), _ -> 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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.12.2 Oracle hint

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

6.12.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.13.2 Oracle hint

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

6.13.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.14.2 Oracle hint

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

6.14.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.15.2 Oracle hint

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

6.15.3 Oracle hint

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

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

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

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

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

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

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

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

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

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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.20.2 Oracle hint

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

6.20.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.21.2 Oracle hint

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

6.21.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.22.2 Oracle hint

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

6.22.3 Oracle hint

[ add1 1 ]
On context:
add1 ({ x -> Top (sign), _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
expr (Top (sign), <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

[ x := (x + 1) ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

6.23.2 Oracle hint

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

6.23.3 Oracle hint

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

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

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

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

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

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

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

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

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

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

6.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>)

7 Running test 6: an unexecuted loop.

7.1 Program

[ while 0
  do x := 42
  od ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

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. (Success)

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

7.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

7.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

7.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

7.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

7.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

7.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

7.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

8 Running test 7: a neverending loop.

8.1 Program

[ while 1
  do x := 42
  od ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

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 := 42 ]
On context:
{ _ -> Undef } | <empty context>, <procedures defined:  > (stat).

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. (Failure)

Failed to get a result.

8.6.1 Failed at

[ x := 42 ]
On context:
{ x -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

8.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

8.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

8.8.1 Failed at

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

8.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

8.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

8.10.1 Failed at

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

8.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

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

Terminated with result: Bot

9 Running test 8: a relatively long computation without loop.

9.1 Program

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

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

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

[ (18 + 17) ]
On context:
{ _ -> Undef } | <empty context> (expr).

9.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

9.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

9.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

9.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

9.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

9.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

9.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

9.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Success)

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

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

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

9.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Success)

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

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

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

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

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

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

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

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

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

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

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

9.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Success)

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

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

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

9.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Success)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

10 Running test 9: a loop terminating after two unfoldings.

10.1 Program

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

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

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. (Failure)

Failed to get a result.

10.4.1 Failed at

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

10.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

10.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

10.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

10.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

10.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

10.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

10.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

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

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

10.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

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

10.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Success)

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

10.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

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

10.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

10.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

10.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

10.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

10.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Success)

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

10.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

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

10.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Success)

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

10.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

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

10.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

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

10.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

10.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

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

10.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

10.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

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

10.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

10.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

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

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

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

10.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

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

10.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

10.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

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

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

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

10.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>)

10.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>)

10.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>)

10.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>)

10.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>)

10.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>)

10.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>)

10.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>)

11 Running test 10: a loop terminating after four unfoldings.

11.1 Program

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

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

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

[ 1 ]
On context:
{ _ -> Undef } | <empty context> (expr).

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. (Failure)

Failed to get a result.

11.8.1 Failed at

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

11.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

Terminated with result: stat ({ _ -> Top (valvar) }, <may be an 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

[ z := 0 ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

11.12.2 Oracle hint

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

11.12.3 Oracle hint

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

[ z := 0 ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

11.14.2 Oracle hint

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

11.14.3 Oracle hint

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

[ z := 0 ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

11.20.2 Oracle hint

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

11.20.3 Oracle hint

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

[ z := 0 ]
On context:
{ z -> +, y -> +, x -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).

11.22.2 Oracle hint

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

11.22.3 Oracle hint

[ y (:=)1 ]
On context:
asgn1 ({ z -> +, y -> +, x -> +, _ -> Undef } | <empty context>, expr (+, <no error>)).
With result:
stat ({ z -> +, y -> +, 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: testing [if] and [throw].

12.1 Program

[ if x
   then throw
   else skip
  fi ; ]

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

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. (Success)

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

12.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

12.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

12.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

12.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

12.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

12.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

12.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

12.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Success)

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

12.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

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

12.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Success)

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

12.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

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

12.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

12.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

12.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

12.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

12.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Success)

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

12.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

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

12.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Success)

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

12.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

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

12.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

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

12.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

12.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

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

12.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

12.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

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

12.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

12.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

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

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

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

12.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

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

12.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

12.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

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

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

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

12.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Success)

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

12.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

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

12.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Success)

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

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

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

12.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Success)

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

12.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Success)

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

13 Running test 12: a loop terminating after four unfoldings with tests.

13.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 } | <empty context>, <procedures defined: > (prog).

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

[ 1 ]
On context:
{ _ -> Undef } | <empty context> (expr).

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. (Success)

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

13.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

13.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

13.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

13.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

13.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

Terminated with result: stat ({ z -> 0, y -> 0, x -> 0, _ -> Undef }, <no 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:
{ z -> 0, y -> +, x -> +, _ -> Undef } | <empty context> (expr).

13.12.2 Oracle hint

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

13.12.3 Oracle hint

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

13.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>)

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:
{ z -> 0, y -> +, x -> +, _ -> Undef } | <empty context> (expr).

13.14.2 Oracle hint

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

13.14.3 Oracle hint

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

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

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:
{ z -> 0, y -> +, x -> +, _ -> Undef } | <empty context> (expr).

13.20.2 Oracle hint

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

13.20.3 Oracle hint

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

13.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>)

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:
{ z -> 0, y -> +, x -> +, _ -> Undef } | <empty context> (expr).

13.22.2 Oracle hint

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

13.22.3 Oracle hint

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

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

13.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>)

14 Running test 13: nested loops.

14.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 } | <empty context>, <procedures defined: > (prog).

14.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

14.3 Running analyser: sign_type_analyse. (Success)

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

14.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

14.4.1 Failed at

[ while1 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:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

14.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

14.6.1 Failed at

[ c ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context> (expr).

14.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

14.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

14.8.1 Failed at

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

14.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

14.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

14.10.1 Failed at

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

14.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

14.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

14.12.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.12.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Failure)

Failed to get a result.

14.13.1 Failed at

[ add1 -1 ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).

14.13.2 Oracle hint

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

14.13.3 Oracle hint

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

14.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

14.14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.14.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Failure)

Failed to get a result.

14.15.1 Failed at

[ add1 -1 ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).

14.15.2 Oracle hint

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

14.15.3 Oracle hint

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

14.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Failure)

Failed to get a result.

14.16.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.16.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Failure)

Failed to get a result.

14.17.1 Failed at

[ (x + c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } | <empty context> (expr).

14.17.2 Oracle hint

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

14.17.3 Oracle hint

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

14.17.4 Oracle hint

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

14.17.5 Oracle hint

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

14.17.6 Oracle hint

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

14.17.7 Oracle hint

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

14.17.8 Oracle hint

[ c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.17.9 Oracle hint

[ x := (x + c) ;
  c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.17.10 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.17.11 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Failure)

Failed to get a result.

14.18.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.18.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Failure)

Failed to get a result.

14.19.1 Failed at

[ (x + c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } | <empty context> (expr).

14.19.2 Oracle hint

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

14.19.3 Oracle hint

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

14.19.4 Oracle hint

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

14.19.5 Oracle hint

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

14.19.6 Oracle hint

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

14.19.7 Oracle hint

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

14.19.8 Oracle hint

[ c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.19.9 Oracle hint

[ x := (x + c) ;
  c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.19.10 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.19.11 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

14.20.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.20.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Failure)

Failed to get a result.

14.21.1 Failed at

[ add1 -1 ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).

14.21.2 Oracle hint

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

14.21.3 Oracle hint

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

14.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

14.22.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.22.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Failure)

Failed to get a result.

14.23.1 Failed at

[ add1 -1 ]
On context:
add1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).

14.23.2 Oracle hint

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

14.23.3 Oracle hint

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

14.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Failure)

Failed to get a result.

14.24.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.24.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Failure)

Failed to get a result.

14.25.1 Failed at

[ (x + c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } | <empty context> (expr).

14.25.2 Oracle hint

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

14.25.3 Oracle hint

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

14.25.4 Oracle hint

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

14.25.5 Oracle hint

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

14.25.6 Oracle hint

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

14.25.7 Oracle hint

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

14.25.8 Oracle hint

[ c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.25.9 Oracle hint

[ x := (x + c) ;
  c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.25.10 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.25.11 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Failure)

Failed to get a result.

14.26.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).

14.26.2 Oracle hint

[ while1 b
  do c := 5 ;
     while c
     do x := (x + c) ;
        c := (c + -1)
     od ;
     b := (b + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>).

14.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Failure)

Failed to get a result.

14.27.1 Failed at

[ (x + c) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef } | <empty context> (expr).

14.27.2 Oracle hint

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

14.27.3 Oracle hint

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

14.27.4 Oracle hint

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

14.27.5 Oracle hint

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

14.27.6 Oracle hint

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

14.27.7 Oracle hint

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

14.27.8 Oracle hint

[ c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.27.9 Oracle hint

[ x := (x + c) ;
  c := (c + -1) ]
On context:
{ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, <procedures defined:  > (stat).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.27.10 Oracle hint

[ x (:=)1 ]
On context:
asgn1 ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef } | <empty context>, expr (Top (sign), <no error>)).
With result:
stat ({ x -> Top (sign), c -> Top (sign), b -> +, a -> +, _ -> Undef }, <no error>).

14.27.11 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.28.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.28.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.29.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.29.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.30.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.30.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.31 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 3 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.31.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.31.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.32.5 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.32.6 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.32.7 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.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>)

14.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.34.5 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.34.6 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.34.7 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.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>)

14.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.36.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.36.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.37.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.37.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.38.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.38.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.39 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.39.2 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.39.3 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.40.5 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.40.6 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.40.7 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.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>)

14.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Failure)

Failed to get a result.

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> +, _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, stat ({ x -> Top (sign), c -> Top (sign), b -> Top (sign), a -> Top (sign), _ -> Undef }, <no error>)).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.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 (<empty context>, <procedures defined:  >, 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>).

14.42.5 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.42.6 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.42.7 Oracle hint

[ while1 c
  do x := (x + c) ;
     c := (c + -1)
  od ]
On context:
while1 (<empty context>, <procedures defined:  >, 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>).

14.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>)

15 Running test 14: a loop whose termination is difficult to tell.

15.1 Program

[ y := 0 ;
  x := 18 ;
  while x
  do x := (x + -1) ;
     y := (y + 1)
  od ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

15.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

15.3 Running analyser: sign_type_analyse. (Success)

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

15.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

15.4.1 Failed at

[ 0 ]
On context:
{ _ -> Undef } | <empty context> (expr).

15.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

15.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

15.6.1 Failed at

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

15.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

15.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

15.8.1 Failed at

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

15.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

15.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

15.10.1 Failed at

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

15.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

15.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

15.12.1 Failed at

[ y ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.12.2 Oracle hint

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

15.12.3 Oracle hint

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

15.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Failure)

Failed to get a result.

15.13.1 Failed at

[ y ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.13.2 Oracle hint

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

15.13.3 Oracle hint

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

15.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

15.14.1 Failed at

[ y ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.14.2 Oracle hint

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

15.14.3 Oracle hint

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

15.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Failure)

Failed to get a result.

15.15.1 Failed at

[ y ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.15.2 Oracle hint

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

15.15.3 Oracle hint

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

15.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

15.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

15.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

15.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

15.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

15.20.1 Failed at

[ y ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.20.2 Oracle hint

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

15.20.3 Oracle hint

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

15.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Failure)

Failed to get a result.

15.21.1 Failed at

[ y ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.21.2 Oracle hint

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

15.21.3 Oracle hint

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

15.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

15.22.1 Failed at

[ y ]
On context:
{ y -> 0, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.22.2 Oracle hint

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

15.22.3 Oracle hint

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

15.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Failure)

Failed to get a result.

15.23.1 Failed at

[ y ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | <empty context> (expr).

15.23.2 Oracle hint

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

15.23.3 Oracle hint

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

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

15.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>)

16 Running test 15: looping by procedures.

16.1 Program

[ f ( x ) := {
    g ( 1 )
  } ;
  g ( x ) := {
    h ( x )
  } ;
  h ( y ) := {
    f ( x )
  } ;
  x := 0 ;
  g ( -1 ) ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

16.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

16.3 Running analyser: sign_type_analyse. (Success)

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

16.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

16.4.1 Failed at

[ x := 0 ;
  g ( -1 ) ]
On context:
{ _ -> Undef } | <empty context>, <procedures defined: f, g, h > (stat).

16.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

16.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

16.6.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : +0 >, <procedures defined: f, g, h > (stat).

16.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

16.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

16.8.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

16.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

16.10.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : + >, <procedures defined: f, g, h >, expr (+0, <no error>)).

16.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

16.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

16.12.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.12.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

Terminated with result: Bot

16.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

16.14.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.14.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

Terminated with result: Bot

16.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Failure)

Failed to get a result.

16.16.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.16.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

Terminated with result: Bot

16.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Failure)

Failed to get a result.

16.18.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.18.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

Terminated with result: Bot

16.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

16.20.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.20.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

Terminated with result: Bot

16.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

16.22.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.22.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

Terminated with result: Bot

16.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Failure)

Failed to get a result.

16.24.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.24.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

Terminated with result: Bot

16.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Failure)

Failed to get a result.

16.26.1 Failed at

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).

16.26.2 Oracle hint

[ f ( x ) ]
On context:
{ x -> 0, _ -> Undef } | < y : -0 >, <procedures defined: f, g, h > (stat).
With result:
Bot.

16.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

Terminated with result: Bot

16.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Failure)

Failed to get a result.

16.28.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.28.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

16.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

Terminated with result: Bot

16.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Failure)

Failed to get a result.

16.30.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.30.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

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

Terminated with result: Bot

16.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Failure)

Failed to get a result.

16.32.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.32.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

16.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

Terminated with result: Bot

16.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Failure)

Failed to get a result.

16.34.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.34.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

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

Terminated with result: Bot

16.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Failure)

Failed to get a result.

16.36.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.36.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

16.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

Terminated with result: Bot

16.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Failure)

Failed to get a result.

16.38.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.38.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

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

Terminated with result: Bot

16.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Failure)

Failed to get a result.

16.40.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.40.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

16.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

Terminated with result: Bot

16.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Failure)

Failed to get a result.

16.42.1 Failed at

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).

16.42.2 Oracle hint

[ call1 h ]
On context:
call1 ({ x -> 0, _ -> Undef } | < x : - >, <procedures defined: f, g, h >, expr (-0, <no error>)).
With result:
Bot.

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

Terminated with result: Bot

17 Running test 16: a triangular sum using procedures.

17.1 Program

[ triangle ( x ) := {
    if x
     then triangle ( (x + -1) ) ;
          res := (res + x)
     else res := 0
    fi
  } ;
  triangle ( 42 ) ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

17.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

17.3 Running analyser: sign_type_analyse. (Success)

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

17.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

17.4.1 Failed at

[ if x
   then triangle ( (x + -1) ) ;
        res := (res + x)
   else res := 0
  fi ]
On context:
{ _ -> Undef } | < x : + >, <procedures defined: triangle > (stat).

17.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

17.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

17.6.1 Failed at

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

17.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

17.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

17.8.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

17.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

17.10.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : Top (sign) >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

17.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

17.12.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.12.2 Oracle hint

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

17.12.3 Oracle hint

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

17.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Failure)

Failed to get a result.

17.13.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.13.2 Oracle hint

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

17.13.3 Oracle hint

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

17.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

17.14.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.14.2 Oracle hint

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

17.14.3 Oracle hint

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

17.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Failure)

Failed to get a result.

17.15.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.15.2 Oracle hint

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

17.15.3 Oracle hint

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

17.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

17.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

17.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

17.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

17.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

17.20.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.20.2 Oracle hint

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

17.20.3 Oracle hint

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

17.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Failure)

Failed to get a result.

17.21.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.21.2 Oracle hint

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

17.21.3 Oracle hint

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

17.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

17.22.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.22.2 Oracle hint

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

17.22.3 Oracle hint

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

17.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Failure)

Failed to get a result.

17.23.1 Failed at

[ x ]
On context:
{ _ -> Undef } | < x : Top (sign) > (expr).

17.23.2 Oracle hint

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

17.23.3 Oracle hint

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

17.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

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

17.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

17.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

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

17.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

17.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Failure)

Failed to get a result.

17.28.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.28.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

17.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

17.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Failure)

Failed to get a result.

17.30.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.30.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

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

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

17.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Failure)

Failed to get a result.

17.32.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.32.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

17.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

17.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Failure)

Failed to get a result.

17.34.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.34.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

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

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

17.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Failure)

Failed to get a result.

17.36.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.36.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

17.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

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

17.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Failure)

Failed to get a result.

17.38.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.38.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

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

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

17.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Failure)

Failed to get a result.

17.40.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.40.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

17.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

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

17.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Failure)

Failed to get a result.

17.42.1 Failed at

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).

17.42.2 Oracle hint

[ call1 triangle ]
On context:
call1 ({ _ -> Undef } | < x : + >, <procedures defined: triangle >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> Top (sign), _ -> Undef }, <no error>).

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

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

18 Running test 17: mixing the two loop causes.

18.1 Program

[ f ( l ) := {
    while y
    do y := (y + -1) ;
       if x
        then f ( 42 )
        else skip
       fi
    od
  } ;
  y := 42 ;
  f ( 18 ) ; ]

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

18.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

18.3 Running analyser: sign_type_analyse. (Success)

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

18.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

18.4.1 Failed at

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

18.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

18.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

18.6.1 Failed at

[ y := (y + -1) ]
On context:
{ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).

18.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

18.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

18.8.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

18.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

18.10.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

18.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

18.12.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.12.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.12.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Failure)

Failed to get a result.

18.13.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.13.2 Oracle hint

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

18.13.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

18.14.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.14.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.14.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Failure)

Failed to get a result.

18.15.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.15.2 Oracle hint

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

18.15.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Failure)

Failed to get a result.

18.16.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.16.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.16.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Failure)

Failed to get a result.

18.17.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.17.2 Oracle hint

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

18.17.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Failure)

Failed to get a result.

18.18.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.18.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.18.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Failure)

Failed to get a result.

18.19.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.19.2 Oracle hint

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

18.19.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

18.20.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.20.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.20.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Failure)

Failed to get a result.

18.21.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.21.2 Oracle hint

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

18.21.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

18.22.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.22.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.22.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Failure)

Failed to get a result.

18.23.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.23.2 Oracle hint

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

18.23.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Failure)

Failed to get a result.

18.24.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.24.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.24.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Failure)

Failed to get a result.

18.25.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.25.2 Oracle hint

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

18.25.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Failure)

Failed to get a result.

18.26.1 Failed at

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).

18.26.2 Oracle hint

[ y := (y + -1) ]
On context:
{ y -> +, x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f > (stat).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.26.3 Oracle hint

[ (;)1
  if x
   then f ( 42 )
   else skip
  fi ]
On context:
seq1 (< l : + >, <procedures defined: f >, stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Failure)

Failed to get a result.

18.27.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.27.2 Oracle hint

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

18.27.3 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Failure)

Failed to get a result.

18.28.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.28.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Failure)

Failed to get a result.

18.29.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.29.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Failure)

Failed to get a result.

18.30.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.30.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.31 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 3 2. (Failure)

Failed to get a result.

18.31.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.31.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Failure)

Failed to get a result.

18.32.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.32.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Failure)

Failed to get a result.

18.33.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.33.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Failure)

Failed to get a result.

18.34.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.34.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.35 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 3 10. (Failure)

Failed to get a result.

18.35.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.35.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Failure)

Failed to get a result.

18.36.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.36.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Failure)

Failed to get a result.

18.37.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.37.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Failure)

Failed to get a result.

18.38.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.38.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.39 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 2. (Failure)

Failed to get a result.

18.39.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.39.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Failure)

Failed to get a result.

18.40.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.40.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Failure)

Failed to get a result.

18.41.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.41.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Failure)

Failed to get a result.

18.42.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.42.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

18.43 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 3 10. (Failure)

Failed to get a result.

18.43.1 Failed at

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).

18.43.2 Oracle hint

[ call1 f ]
On context:
call1 ({ y -> Top (sign), x -> Top (sign), _ -> Undef } | < l : + >, <procedures defined: f >, expr (+, <no error>)).
With result:
stat ({ y -> Top (sign), x -> Top (sign), _ -> Undef }, <no error>).

19 Running test 18: 6 × 7 using procedures.

19.1 Program

[ prod ( n ) := {
    if n
     then prod ( (n + -1) ) ;
          res := (res + b)
     else res := 0
    fi
  } ;
  a := 6 ;
  b := 7 ;
  prod ( a ) ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

19.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

19.3 Running analyser: sign_type_analyse. (Success)

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

19.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

19.4.1 Failed at

[ a := 6 ]
On context:
{ _ -> Undef } | <empty context>, <procedures defined: prod > (stat).

19.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

19.6 Running analyser: sign_analyse_fuel_fail 100. (Failure)

Failed to get a result.

19.6.1 Failed at

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

19.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

19.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Failure)

Failed to get a result.

19.8.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

19.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Failure)

Failed to get a result.

19.10.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : Top (sign) >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

19.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

19.12.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.12.2 Oracle hint

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

19.12.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

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

19.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

19.14.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.14.2 Oracle hint

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

19.14.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

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

19.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Failure)

Failed to get a result.

19.16.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.16.2 Oracle hint

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

19.16.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

19.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Failure)

Failed to get a result.

19.18.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.18.2 Oracle hint

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

19.18.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

19.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

19.20.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.20.2 Oracle hint

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

19.20.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

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

19.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

19.22.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.22.2 Oracle hint

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

19.22.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

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

19.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Failure)

Failed to get a result.

19.24.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.24.2 Oracle hint

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

19.24.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

19.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Failure)

Failed to get a result.

19.26.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.26.2 Oracle hint

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

19.26.3 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

19.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Failure)

Failed to get a result.

19.28.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.28.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

19.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Failure)

Failed to get a result.

19.30.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.30.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

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

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

19.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Failure)

Failed to get a result.

19.32.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.32.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

19.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Failure)

Failed to get a result.

19.34.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.34.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

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

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

19.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Failure)

Failed to get a result.

19.36.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.36.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

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

19.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Failure)

Failed to get a result.

19.38.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.38.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

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

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

19.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Failure)

Failed to get a result.

19.40.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.40.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

19.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

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

19.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Failure)

Failed to get a result.

19.42.1 Failed at

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).

19.42.2 Oracle hint

[ call1 prod ]
On context:
call1 ({ b -> +, a -> +, _ -> Undef } | < n : + >, <procedures defined: prod >, expr (Top (sign), <no error>)).
With result:
stat ({ res -> +0, b -> +, a -> +, _ -> Undef }, <no error>).

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

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

20 Running test 19: an identity function used more than one time with different values.

20.1 Program

[ id ( x ) := {
    res := x
  } ;
  id ( 42 ) ;
  r1 := res ;
  id ( -1 ) ;
  r2 := res ;
  id ( 0 ) ;
  r3 := res ;
  id ( 18 ) ;
  id ( res ) ;
  id ( res ) ;
  r4 := res ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

20.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

20.3 Running analyser: sign_type_analyse. (Success)

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

20.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

20.4.1 Failed at

[ id ( 42 ) ]
On context:
{ _ -> Undef } | <empty context>, <procedures defined: id > (stat).

20.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

20.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

20.12.1 Failed at

[ r3 (:=)1 ]
On context:
asgn1 ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context>, expr (0, <no error>)).

20.12.2 Oracle hint

[ res ]
On context:
{ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context> (expr).
With result:
expr (0, <no error>).

20.12.3 Oracle hint

[ res := x ]
On context:
{ res -> -, r2 -> -, r1 -> +, _ -> Undef } | < x : 0 >, <procedures defined: id > (stat).
With result:
stat ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>).

20.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

20.14.1 Failed at

[ r3 (:=)1 ]
On context:
asgn1 ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context>, expr (0, <no error>)).

20.14.2 Oracle hint

[ res ]
On context:
{ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context> (expr).
With result:
expr (0, <no error>).

20.14.3 Oracle hint

[ res := x ]
On context:
{ res -> -, r2 -> -, r1 -> +, _ -> Undef } | < x : 0 >, <procedures defined: id > (stat).
With result:
stat ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>).

20.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

20.20.1 Failed at

[ r3 (:=)1 ]
On context:
asgn1 ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context>, expr (0, <no error>)).

20.20.2 Oracle hint

[ res ]
On context:
{ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context> (expr).
With result:
expr (0, <no error>).

20.20.3 Oracle hint

[ res := x ]
On context:
{ res -> -, r2 -> -, r1 -> +, _ -> Undef } | < x : 0 >, <procedures defined: id > (stat).
With result:
stat ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>).

20.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

20.22.1 Failed at

[ r3 (:=)1 ]
On context:
asgn1 ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context>, expr (0, <no error>)).

20.22.2 Oracle hint

[ res ]
On context:
{ res -> 0, r2 -> -, r1 -> +, _ -> Undef } | <empty context> (expr).
With result:
expr (0, <no error>).

20.22.3 Oracle hint

[ res := x ]
On context:
{ res -> -, r2 -> -, r1 -> +, _ -> Undef } | < x : 0 >, <procedures defined: id > (stat).
With result:
stat ({ res -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>).

20.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

20.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Success)

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> +, r4 -> +, r3 -> 0, r2 -> -, r1 -> +, _ -> Undef }, <no error>)

21 Running test 20: variation of the previous example.

21.1 Program

[ f ( x ) := {
    if x
     then res := 0
     else res := x
    fi
  } ;
  f ( 42 ) ;
  r1 := res ;
  f ( -1 ) ;
  r2 := res ;
  f ( 0 ) ;
  r3 := res ;
  f ( 18 ) ;
  f ( res ) ;
  f ( res ) ;
  r4 := res ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

21.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

21.3 Running analyser: sign_type_analyse. (Success)

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

21.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

21.4.1 Failed at

[ f ( 42 ) ]
On context:
{ _ -> Undef } | <empty context>, <procedures defined: f > (stat).

21.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

21.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Failure)

Failed to get a result.

21.12.1 Failed at

[ res ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | <empty context> (expr).

21.12.2 Oracle hint

[ res := 0 ]
On context:
{ res -> 0, r1 -> 0, _ -> Undef } | < x : - >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.12.3 Oracle hint

[ if x
   then res := 0
   else res := x
  fi ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | < x : 0 >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Failure)

Failed to get a result.

21.14.1 Failed at

[ res ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | <empty context> (expr).

21.14.2 Oracle hint

[ res := 0 ]
On context:
{ res -> 0, r1 -> 0, _ -> Undef } | < x : - >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.14.3 Oracle hint

[ if x
   then res := 0
   else res := x
  fi ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | < x : 0 >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Failure)

Failed to get a result.

21.20.1 Failed at

[ res ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | <empty context> (expr).

21.20.2 Oracle hint

[ res := 0 ]
On context:
{ res -> 0, r1 -> 0, _ -> Undef } | < x : - >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.20.3 Oracle hint

[ if x
   then res := 0
   else res := x
  fi ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | < x : 0 >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Failure)

Failed to get a result.

21.22.1 Failed at

[ res ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | <empty context> (expr).

21.22.2 Oracle hint

[ res := 0 ]
On context:
{ res -> 0, r1 -> 0, _ -> Undef } | < x : - >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.22.3 Oracle hint

[ if x
   then res := 0
   else res := x
  fi ]
On context:
{ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef } | < x : 0 >, <procedures defined: f > (stat).
With result:
stat ({ res -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>).

21.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

21.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Success)

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

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

Terminated with result: stat ({ res -> 0, r4 -> 0, r3 -> 0, r2 -> 0, r1 -> 0, _ -> Undef }, <no error>)

22 Running test 21: calling an undefined procedure.

22.1 Program

[ undefined_proc ( 42 ) ; ]

On context: { _ -> Undef } | <empty context>, <procedures defined: > (prog).

22.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

22.3 Running analyser: sign_type_analyse. (Success)

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

22.4 Running analyser: sign_analyse_fuel_fail 4. (Success)

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

22.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

22.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

22.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

22.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

22.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

22.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

22.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

22.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Success)

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

22.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

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

22.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Success)

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

22.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

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

22.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

22.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

22.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

22.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

22.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Success)

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

22.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

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

22.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Success)

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

22.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

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

22.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

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

22.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

22.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

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

22.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

22.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

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

22.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

22.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

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

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

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

22.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

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

22.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

22.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

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

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

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

22.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>)

22.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>)

22.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>)

22.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>)

22.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>)

22.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>)

22.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>)

22.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>)

23 Running test 22: a relationnal example (the current lattices are not adapted for this example).

23.1 Program

[ if x
   then y := -1
   else y := 1
  fi ;
  if y
   then if x
         then z := 1
         else z := -1
        fi
   else throw
  fi ;
  if (y + z)
   then a := 1
   else a := 0
  fi ; ]

On context: { x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined: > (prog).

23.2 Running analyser: sign_trivial_analyser. (Success)

Terminated with result: Top

23.3 Running analyser: sign_type_analyse. (Success)

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

23.4 Running analyser: sign_analyse_fuel_fail 4. (Failure)

Failed to get a result.

23.4.1 Failed at

[ y := -1 ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

23.4.2 Failed at

[ y := 1 ]
On context:
{ x -> Top (sign), _ -> Undef } | <empty context>, <procedures defined:  > (stat).

23.5 Running analyser: sign_analyse_fuel type_analyse 4. (Success)

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

23.6 Running analyser: sign_analyse_fuel_fail 100. (Success)

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

23.7 Running analyser: sign_analyse_fuel type_analyse 100. (Success)

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

23.8 Running analyser: sign_analyse_deep_fuel_fail 1. (Success)

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

23.9 Running analyser: sign_analyse_deep_fuel type_analyse 1. (Success)

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

23.10 Running analyser: sign_analyse_deep_fuel_fail 10. (Success)

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

23.11 Running analyser: sign_analyse_deep_fuel type_analyse 10. (Success)

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

23.12 Running analyser: sign_analyse_oracle_back_and_forth 10 1 2. (Success)

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

23.13 Running analyser: sign_analyse_oracle_back_and_forth 50 1 2. (Success)

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

23.14 Running analyser: sign_analyse_oracle_back_and_forth 10 3 2. (Success)

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

23.15 Running analyser: sign_analyse_oracle_back_and_forth 50 3 2. (Success)

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

23.16 Running analyser: sign_analyse_oracle_back_and_forth 10 1 10. (Success)

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

23.17 Running analyser: sign_analyse_oracle_back_and_forth 50 1 10. (Success)

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

23.18 Running analyser: sign_analyse_oracle_back_and_forth 10 3 10. (Success)

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

23.19 Running analyser: sign_analyse_oracle_back_and_forth 50 3 10. (Success)

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

23.20 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 2. (Success)

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

23.21 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 2. (Success)

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

23.22 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 2. (Success)

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

23.23 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 2. (Success)

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

23.24 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 1 10. (Success)

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

23.25 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 1 10. (Success)

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

23.26 Running analyser: sign_analyse_oracle_back_and_forth_loop 10 3 10. (Success)

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

23.27 Running analyser: sign_analyse_oracle_back_and_forth_loop 50 3 10. (Success)

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

23.28 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 2. (Success)

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

23.29 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 2. (Success)

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

23.30 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 2. (Success)

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

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

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

23.32 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 1 10. (Success)

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

23.33 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 5 1 10. (Success)

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

23.34 Running analyser: sign_analyse_oracle_back_and_forth_deep 1 1 3 10. (Success)

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

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

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

23.36 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 2. (Success)

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

23.37 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 2. (Success)

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

23.38 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 2. (Success)

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

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

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

23.40 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 1 10. (Success)

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

23.41 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 5 1 10. (Success)

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

23.42 Running analyser: sign_analyse_oracle_back_and_forth_deep_loop 1 1 3 10. (Success)

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

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

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