warning: Ignored call to evalwcet1stop/4 in equation evalwcet1returnin/4 
Inferred cost of evalwcet1bbin(A,B,C,D,E,F,G,H,I): 
evalwcet1bbin(A,B,C,D,E,F,G,H,I):[24]: 3
  with precondition: [A=1,B=0,C=1,E=0,F=1,G=0,H=1,I=0] 

evalwcet1bbin(A,B,C,D,E,F,G,H,I):[26]: 4
  with precondition: [A=1,B=0,C=1,E=0,F=1,G=0,H=1,I=0] 

evalwcet1bbin(A,B,C,D,E,F,G,H,I):[[21,22,23],24]: 3+it1*(4)+it2*(3)
  Such that:it1+it2=<1*G,it1+it2=<1*C+ -1,it1+it2=<1*F+ -1,it1+it2=<1*G+ -1*B,it1+it2=<1*A+ -1*B+ -1
  with precondition: [E=0,H=1,I=0,A=F,A=G+1,A=B+C,B>=0,A>=B+2] 

evalwcet1bbin(A,B,C,D,E,F,G,H,I):[[21,22,23],25]: 3+it1*(4)+it2*(3)
  Such that:it1+it2=<1*C+ -1,it1+it2=<1*F+ -1,it1+it2=<-1*B+1*A+ -1,it1+it2=<-1*B+1*F+ -1
  with precondition: [E=0,H=1,A=F,G+1=I,B>=0,C>=2,G>=0,A>=G+2,A>=B+C,C+G>=B+1,B+C>=G+1] 

evalwcet1bbin(A,B,C,D,E,F,G,H,I):[[21,22,23],26]: 4+it1*(4)+it2*(3)
  Such that:it1+it2=<1*C+ -1,it1+it2=<1*F+ -1,it1+it2=<-1*B+1*A+ -1,it1+it2=<-1*B+1*F+ -1
  with precondition: [E=0,H=1,I=0,A=F,1>=G,B>=0,C>=2,G>=0,A>=B+C,C+G>=B+1] 

evalwcet1bbin(A,B,C,D,E,F,G,H,I):[[21,22,23],27]: 3+it1*(4)+it2*(3)
  Such that:it1+it2=<1*C+ -1,it1+it2=<1*F+ -1,it1+it2=<-1*B+1*A+ -1,it1+it2=<-1*B+1*F+ -1
  with precondition: [E=0,H=1,A=F,G=I+1,B>=0,C>=2,G>=2,A>=B+C,C+G>=B+1,B+C>=G+1] 

Inferred cost of evalwcet1returnin(A,B,C,D): 
evalwcet1returnin(A,B,C,D):[29]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalwcet1bbin(A,B,C,D): 
loop_cont_evalwcet1bbin(A,B,C,D):[31]: 1
  with precondition: [] 

Inferred cost of evalwcet1entryin(A,B,C,D): 
evalwcet1entryin(A,B,C,D):[33]: 2
  with precondition: [0>=A] 

evalwcet1entryin(A,B,C,D):[34]: 5
  with precondition: [A=1] 

evalwcet1entryin(A,B,C,D):[35]: 6
  with precondition: [A=1] 

evalwcet1entryin(A,B,C,D):[36]: 5+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1entryin(A,B,C,D):[37]: 5+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1entryin(A,B,C,D):[38]: 6+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1entryin(A,B,C,D):[39]: 5+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=3] 

Inferred cost of evalwcet1start(A,B,C,D): 
evalwcet1start(A,B,C,D):[41]: 3
  with precondition: [0>=A] 

evalwcet1start(A,B,C,D):[42]: 6
  with precondition: [A=1] 

evalwcet1start(A,B,C,D):[43]: 7
  with precondition: [A=1] 

evalwcet1start(A,B,C,D):[44]: 6+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1start(A,B,C,D):[45]: 6+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1start(A,B,C,D):[46]: 7+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=2] 

evalwcet1start(A,B,C,D):[47]: 6+it1*(4)+it2*(3)
  Such that:it1+it2=<1*A+ -1
  with precondition: [A>=3] 

Solved cost expressions of evalwcet1start(A,B,C,D): 
evalwcet1start(A,B,C,D):[41]: 3  with precondition: [0>=A] 
evalwcet1start(A,B,C,D):[42]: 6  with precondition: [A=1] 
evalwcet1start(A,B,C,D):[43]: 7  with precondition: [A=1] 
evalwcet1start(A,B,C,D):[44]: 4*A+2  with precondition: [A>=2] 
evalwcet1start(A,B,C,D):[45]: 4*A+2  with precondition: [A>=2] 
evalwcet1start(A,B,C,D):[46]: 4*A+3  with precondition: [A>=2] 
evalwcet1start(A,B,C,D):[47]: 4*A+2  with precondition: [A>=3] 
Maximum cost of evalwcet1start(A,B,C,D): max([4*A+3,7]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 23 ms.
Invariants computed in 53 ms.
----Backward Invariants 35 ms.
----Transitive Invariants 4 ms.
Refinement performed in 44 ms.
Termination proved in 10 ms.
Upper bounds computed in 69 ms.
----Phase cost structures 21 ms.
--------Equation cost structures 20 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 41 ms.
----Solving cost expressions 2 ms.

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