warning: Ignored call to evalcousot9stop/3 in equation evalcousot9returnin/3 
Inferred cost of evalcousot9bb3in(A,B,C,D,E,F,G): 
evalcousot9bb3in(A,B,C,D,E,F,G):[16]: 1
  with precondition: [D=0,E=A,B=C,B=F,B=G,0>=B] 

evalcousot9bb3in(A,B,C,D,E,F,G):[[14,15],16]: 1+it1*(3)+it2*(3)
  Such that:it1=<nat(min([1*B,1*C,1*G]))*min([1*C,1*G])+1*A,it2=<1*B,it2=<1*C,it2=<1*G,it2=<nat(min([1*B,1*C,1*G]))*min([1*C,1*G])+1*A+ (-1*A+1)
  with precondition: [D=0,F=0,C=E,C=G,B>=1,C>=B] 

Inferred cost of evalcousot9returnin(A,B,C): 
evalcousot9returnin(A,B,C):[18]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalcousot9bb3in(A,B,C): 
loop_cont_evalcousot9bb3in(A,B,C):[20]: 1
  with precondition: [] 

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

evalcousot9entryin(A,B,C):[23]: inf
  with precondition: [C>=1] 

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

evalcousot9start(A,B,C):[26]: inf
  with precondition: [C>=1] 

Solved cost expressions of evalcousot9start(A,B,C): 
evalcousot9start(A,B,C):[25]: 4  with precondition: [0>=C] 
evalcousot9start(A,B,C):[26]: inf  with precondition: [C>=1] 
Maximum cost of evalcousot9start(A,B,C): inf 
Asymptotic class: infinity 
Time statistics: 
Partial evaluation computed in 7 ms.
Invariants computed in 13 ms.
----Backward Invariants 6 ms.
----Transitive Invariants 2 ms.
Refinement performed in 14 ms.
Termination proved in 5 ms.
Upper bounds computed in 28 ms.
----Phase cost structures 10 ms.
--------Equation cost structures 7 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 15 ms.
----Solving cost expressions 0 ms.

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