warning: Ignored call to evalndloopstop/1 in equation evalndloopreturnin/1 
Inferred cost of evalndloopbbin(A,B,C): 
evalndloopbbin(A,B,C):[19]: 1
  with precondition: [A=0,B=0,C=0] 

evalndloopbbin(A,B,C):[20]: 0
  with precondition: [A=0,B=1,C=0] 

evalndloopbbin(A,B,C):[21]: 1
  with precondition: [A=0,B=0,C=0] 

evalndloopbbin(A,B,C):[22]: 0
  with precondition: [A=0,B=1,C=0] 

evalndloopbbin(A,B,C):[23]: 1
  with precondition: [A=0,B=0,C=0] 

evalndloopbbin(A,B,C):[24]: 0
  with precondition: [A=0,B=1,C=0] 

evalndloopbbin(A,B,C):[[18],19]: 1+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=0,9>=C,A>=0,C>=A+1] 

evalndloopbbin(A,B,C):[[18],20]: 0+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=1,9>=C,A>=0,C>=A+1] 

evalndloopbbin(A,B,C):[[18],21]: 1+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=0,9>=C,A>=0,C>=A+1] 

evalndloopbbin(A,B,C):[[18],22]: 0+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=1,9>=C,A>=0,C>=A+1] 

evalndloopbbin(A,B,C):[[18],23]: 1+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=0,9>=C,A>=0,C>=A+1] 

evalndloopbbin(A,B,C):[[18],24]: 0+it1*(1)
  Such that:it1=<9,it1=<1*C,it1=<-1*A+9,it1=<1*C+ -1*A
  with precondition: [B=1,9>=C,A>=0,C>=A+1] 

Inferred cost of evalndloopreturnin(A): 
evalndloopreturnin(A):[26]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalndloopbbin(A): 
loop_cont_evalndloopbbin(A):[28]: 1
  with precondition: [] 

Inferred cost of evalndloopentryin(A): 
evalndloopentryin(A):[30]: 3
  with precondition: [] 

evalndloopentryin(A):[31]: 3
  with precondition: [] 

evalndloopentryin(A):[32]: 3
  with precondition: [] 

evalndloopentryin(A):[33]: 3+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopentryin(A):[34]: 3+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopentryin(A):[35]: 3+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopentryin(A):[36]: 1
  with precondition: [] 

evalndloopentryin(A):[37]: 1
  with precondition: [] 

evalndloopentryin(A):[38]: 1
  with precondition: [] 

evalndloopentryin(A):[39]: 1+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopentryin(A):[40]: 1+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopentryin(A):[41]: 1+it1*(1)
  Such that:it1=<9
  with precondition: [] 

Inferred cost of evalndloopstart(A): 
evalndloopstart(A):[43]: 4
  with precondition: [] 

evalndloopstart(A):[44]: 4
  with precondition: [] 

evalndloopstart(A):[45]: 4
  with precondition: [] 

evalndloopstart(A):[46]: 4+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopstart(A):[47]: 4+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopstart(A):[48]: 4+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopstart(A):[49]: 2
  with precondition: [] 

evalndloopstart(A):[50]: 2
  with precondition: [] 

evalndloopstart(A):[51]: 2
  with precondition: [] 

evalndloopstart(A):[52]: 2+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopstart(A):[53]: 2+it1*(1)
  Such that:it1=<9
  with precondition: [] 

evalndloopstart(A):[54]: 2+it1*(1)
  Such that:it1=<9
  with precondition: [] 

Solved cost expressions of evalndloopstart(A): 
evalndloopstart(A):[43]: 4  with precondition: [] 
evalndloopstart(A):[44]: 4  with precondition: [] 
evalndloopstart(A):[45]: 4  with precondition: [] 
evalndloopstart(A):[46]: 13  with precondition: [] 
evalndloopstart(A):[47]: 13  with precondition: [] 
evalndloopstart(A):[48]: 13  with precondition: [] 
evalndloopstart(A):[49]: 2  with precondition: [] 
evalndloopstart(A):[50]: 2  with precondition: [] 
evalndloopstart(A):[51]: 2  with precondition: [] 
evalndloopstart(A):[52]: 11  with precondition: [] 
evalndloopstart(A):[53]: 11  with precondition: [] 
evalndloopstart(A):[54]: 11  with precondition: [] 
Maximum cost of evalndloopstart(A): 13 
Asymptotic class: constant 
Time statistics: 
Partial evaluation computed in 2 ms.
Invariants computed in 21 ms.
----Backward Invariants 15 ms.
----Transitive Invariants 0 ms.
Refinement performed in 16 ms.
Termination proved in 2 ms.
Upper bounds computed in 38 ms.
----Phase cost structures 12 ms.
--------Equation cost structures 9 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 19 ms.
----Solving cost expressions 0 ms.

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