warning: Ignored call to evalEx3stop/3 in equation evalEx3returnin/3 
Inferred cost of evalEx3bb2in(A,B,C,D,E,F,G): 
evalEx3bb2in(A,B,C,D,E,F,G):[22]: 2
  with precondition: [D=0,F=B,A=C,A=E,A=G,A>=1] 

evalEx3bb2in(A,B,C,D,E,F,G):[23]: 1
  with precondition: [D=1,F=B,A=C,A=E,A=G,A>=1] 

evalEx3bb2in(A,B,C,D,E,F,G):[24]: 2
  with precondition: [D=0,F=B,A=C,A=E,A=G,A>=1] 

evalEx3bb2in(A,B,C,D,E,F,G):[25]: 1
  with precondition: [D=1,F=B,A=C,A=E,A=G,A>=1] 

evalEx3bb2in(A,B,C,D,E,F,G):[[21],22]: 2+it1*(3)
  Such that:it1=<1*A,it1=<1*C,it1=<-1*G+1*A,it1=<1*C+ -1*G
  with precondition: [D=0,G=E,B=F,G>=1,A>=C,C>=G+1] 

evalEx3bb2in(A,B,C,D,E,F,G):[[21],23]: 1+it1*(3)
  Such that:it1=<1*A,it1=<1*C,it1=<1*E,it1=<-1*G+1*A,it1=<-1*G+1*E,it1=<1*C+ -1*G
  with precondition: [D=1,A=E,B=F,G>=1,A>=C,C>=G+1] 

evalEx3bb2in(A,B,C,D,E,F,G):[[21],24]: 2+it1*(3)
  Such that:it1=<1*A,it1=<1*C,it1=<-1*G+1*A,it1=<1*C+ -1*G
  with precondition: [D=0,G=E,B=F,G>=1,A>=C,C>=G+1] 

evalEx3bb2in(A,B,C,D,E,F,G):[[21],25]: 1+it1*(3)
  Such that:it1=<1*A,it1=<1*C,it1=<1*E,it1=<-1*G+1*A,it1=<-1*G+1*E,it1=<1*C+ -1*G
  with precondition: [D=1,A=E,B=F,G>=1,A>=C,C>=G+1] 

evalEx3bb2in(A,B,C,D,E,F,G):[[21],26]: 1+it1*(3)
  Such that:it1=<1*A,it1=<1*C
  with precondition: [D=0,E=0,G=0,B=F,C>=1,A>=C] 

Inferred cost of evalEx3bb4in(A,B,C,D,E,F,G): 
evalEx3bb4in(A,B,C,D,E,F,G):[33]: 3
  with precondition: [D=1,A>=1] 

evalEx3bb4in(A,B,C,D,E,F,G):[34]: 3
  with precondition: [D=1,A>=1] 

evalEx3bb4in(A,B,C,D,E,F,G):[35]: 3+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [D=1,A>=2] 

evalEx3bb4in(A,B,C,D,E,F,G):[36]: 3+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [D=1,A>=2] 

evalEx3bb4in(A,B,C,D,E,F,G):[37]: 1
  with precondition: [D=0,F=B,G=C,A=E,0>=A] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],32,37]: inf
  with precondition: [D=0,E=0,G=0,A>=1] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],33]: inf
  with precondition: [D=1,A>=1] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],34]: inf
  with precondition: [D=1,A>=1] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],35]: inf
  with precondition: [D=1,A>=2] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],36]: inf
  with precondition: [D=1,A>=2] 

evalEx3bb4in(A,B,C,D,E,F,G):[[28,29,30,31],38]...: inf
  with precondition: [1>=D,A>=1,D>=0] 

evalEx3bb4in(A,B,C,D,E,F,G):[32,37]: 4+it1*(3)
  Such that:it1=<1*A
  with precondition: [D=0,E=0,G=0,A>=1] 

Inferred cost of evalEx3returnin(A,B,C): 
evalEx3returnin(A,B,C):[39]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalEx3bb4in(A,B,C): 
loop_cont_evalEx3bb4in(A,B,C):[41]: 1
  with precondition: [] 

Inferred cost of evalEx3entryin(A,B,C): 
evalEx3entryin(A,B,C):[43]: 3
  with precondition: [0>=A] 

evalEx3entryin(A,B,C):[44]: inf
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[45]: 6+it1*(3)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[46]: 4
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[47]: 4
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[48]: 4+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [A>=2] 

evalEx3entryin(A,B,C):[49]: 4+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [A>=2] 

evalEx3entryin(A,B,C):[50]: inf
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[51]: inf
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[52]: inf
  with precondition: [A>=2] 

evalEx3entryin(A,B,C):[53]: inf
  with precondition: [A>=2] 

evalEx3entryin(A,B,C):[54]...: inf
  with precondition: [A>=1] 

evalEx3entryin(A,B,C):[55]...: inf
  with precondition: [A>=1] 

Inferred cost of evalEx3start(A,B,C): 
evalEx3start(A,B,C):[57]: 4
  with precondition: [0>=A] 

evalEx3start(A,B,C):[58]: inf
  with precondition: [A>=1] 

evalEx3start(A,B,C):[59]: 7+it1*(3)
  Such that:it1=<1*A
  with precondition: [A>=1] 

evalEx3start(A,B,C):[60]: 5
  with precondition: [A>=1] 

evalEx3start(A,B,C):[61]: 5
  with precondition: [A>=1] 

evalEx3start(A,B,C):[62]: 5+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [A>=2] 

evalEx3start(A,B,C):[63]: 5+it1*(3)
  Such that:it1=<1*A,it1=<1*A+ -1
  with precondition: [A>=2] 

evalEx3start(A,B,C):[64]: inf
  with precondition: [A>=1] 

evalEx3start(A,B,C):[65]: inf
  with precondition: [A>=1] 

evalEx3start(A,B,C):[66]: inf
  with precondition: [A>=2] 

evalEx3start(A,B,C):[67]: inf
  with precondition: [A>=2] 

evalEx3start(A,B,C):[68]...: inf
  with precondition: [A>=1] 

evalEx3start(A,B,C):[69]...: inf
  with precondition: [A>=1] 

Solved cost expressions of evalEx3start(A,B,C): 
evalEx3start(A,B,C):[57]: 4  with precondition: [0>=A] 
evalEx3start(A,B,C):[58]: inf  with precondition: [A>=1] 
evalEx3start(A,B,C):[59]: 3*A+7  with precondition: [A>=1] 
evalEx3start(A,B,C):[60]: 5  with precondition: [A>=1] 
evalEx3start(A,B,C):[61]: 5  with precondition: [A>=1] 
evalEx3start(A,B,C):[62]: 3*A+2  with precondition: [A>=2] 
evalEx3start(A,B,C):[63]: 3*A+2  with precondition: [A>=2] 
evalEx3start(A,B,C):[64]: inf  with precondition: [A>=1] 
evalEx3start(A,B,C):[65]: inf  with precondition: [A>=1] 
evalEx3start(A,B,C):[66]: inf  with precondition: [A>=2] 
evalEx3start(A,B,C):[67]: inf  with precondition: [A>=2] 
evalEx3start(A,B,C):[68]...: inf  with precondition: [A>=1] 
evalEx3start(A,B,C):[69]...: inf  with precondition: [A>=1] 
Maximum cost of evalEx3start(A,B,C): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 14 ms.
Invariants computed in 67 ms.
----Backward Invariants 43 ms.
----Transitive Invariants 3 ms.
Refinement performed in 49 ms.
Termination proved in 8 ms.
Upper bounds computed in 110 ms.
----Phase cost structures 34 ms.
--------Equation cost structures 30 ms.
--------Inductive compression(1) 2 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 68 ms.
----Solving cost expressions 1 ms.

Compressed phase information: 14 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 270 ms.