warning: Ignored call to evalsipma91stop/4 in equation evalsipma91returnin/4 
Inferred cost of evalsipma91bb3in(A,B,C,D,E,F,G,H,I): 
evalsipma91bb3in(A,B,C,D,E,F,G,H,I):[[23],24]: 1+it1*(2)
  Such that:it1=<-1/11*B+101/11,it1=<1/11*G+ -1/11*B
  with precondition: [E=0,C=H,D=I,G+11*A=11*F+B,111>=G,A>=1,G>=101,G>=B+11] 

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

Inferred cost of evalsipma91bb11in(A,B,C,D,E,F,G,H,I): 
evalsipma91bb11in(A,B,C,D,E,F,G,H,I):[32]: 1
  with precondition: [E=0,G=B,H=C,I=D,A=F,1>=A] 

evalsipma91bb11in(A,B,C,D,E,F,G,H,I):[[28,29,30],31,32]: 3+it1*(3)+it2*(3)
  Such that:it1=<1*A+ -2,it1=<nat(9*A+ -1*B+93)*max([1/9,1/9])+min([1/9*B+ -110/9,1/90*H+1/10*G+1*A+ -1189/90]),it2=<9*A+ -1*B+93,it2=<9*A+1*G+ -1*B+ -8
  with precondition: [E=0,F=1,G+10*I=H+11,G>=101,I>=1,A>=I+1,G+I+9*A>=B+10] 

evalsipma91bb11in(A,B,C,D,E,F,G,H,I):[31,32]: 3
  with precondition: [A=2,E=0,F=1,G+10=B,C=H,D=I,G>=101] 

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

Inferred cost of loop_cont_evalsipma91bb3in(A,B,C,D): 
loop_cont_evalsipma91bb3in(A,B,C,D):[36]: 2
  with precondition: [1>=A] 

loop_cont_evalsipma91bb3in(A,B,C,D):[37]: 4+it1*(3)+it2*(3)
  Such that:it1=<1*A+ -2,it1=<nat(9*A+ -1*B+93)*max([1/9,1/9])+min([1/9*B+ -110/9,inf]),it2=<9*A+ -1*B+93
  with precondition: [A>=2] 

loop_cont_evalsipma91bb3in(A,B,C,D):[38]: 4
  with precondition: [A=2,B>=111] 

Inferred cost of evalsipma91entryin(A,B,C,D): 
evalsipma91entryin(A,B,C,D):[40]: 2
  with precondition: [A>=101] 

evalsipma91entryin(A,B,C,D):[41]: 6+it1*(2)+it2*(3)+it3*(3)
  Such that:it1=<-1/11*A+101/11,it1=<-1/11*A+111/11,it2=<nat(min([-1*A+100,-9/11*A+920/11]))*max([1/9,1/9])+min([1/9,inf]),it2=<-1/11*A+100/11,it3=<-1*A+100,it3=<-9/11*A+920/11
  with precondition: [100>=A] 

evalsipma91entryin(A,B,C,D):[42]: 6+it1*(2)
  Such that:it1=<1,it1=<1/11
  with precondition: [A=100] 

Inferred cost of evalsipma91start(A,B,C,D): 
evalsipma91start(A,B,C,D):[44]: 3
  with precondition: [A>=101] 

evalsipma91start(A,B,C,D):[45]: 7+it1*(2)+it2*(3)+it3*(3)
  Such that:it1=<-1/11*A+101/11,it1=<-1/11*A+111/11,it2=<nat(min([-1*A+100,-9/11*A+920/11]))*max([1/9,1/9])+min([1/9,inf]),it2=<-1/11*A+100/11,it3=<-1*A+100,it3=<-9/11*A+920/11
  with precondition: [100>=A] 

evalsipma91start(A,B,C,D):[46]: 7+it1*(2)
  Such that:it1=<1,it1=<1/11
  with precondition: [A=100] 

Solved cost expressions of evalsipma91start(A,B,C,D): 
evalsipma91start(A,B,C,D):[44]: 3  with precondition: [A>=101] 
evalsipma91start(A,B,C,D):[45]: -2/11*A+202/11+nat(min([-1/11*A+100/11,1/9+1/9*nat(min([-9/11*A+920/11,-1*A+100]))]))*3+nat(min([-9/11*A+920/11,-1*A+100]))*3+7  with precondition: [100>=A] 
evalsipma91start(A,B,C,D):[46]: 79/11  with precondition: [A=100] 
Maximum cost of evalsipma91start(A,B,C,D): max([79/11,-2/11*A+202/11+nat(min([-1/11*A+100/11,1/9+1/9*nat(min([-9/11*A+920/11,-1*A+100]))]))*3+nat(min([-9/11*A+920/11,-1*A+100]))*3+7]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 19 ms.
Invariants computed in 39 ms.
----Backward Invariants 17 ms.
----Transitive Invariants 6 ms.
Refinement performed in 44 ms.
Termination proved in 12 ms.
Upper bounds computed in 60 ms.
----Phase cost structures 26 ms.
--------Equation cost structures 23 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 27 ms.
----Solving cost expressions 2 ms.

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