warning: Ignored call to f3/5 in equation f2/5 warning: Ignored call to loop_cont_f300/5 in equation f2/5 Inferred cost of f300(A,B,C,D,E,F,G,H,I,J,K): f300(A,B,C,D,E,F,G,H,I,J,K):[[8],9]: 1+it1*(1) Such that:it1=<100,it1=<-1*A+101 with precondition: [F=1,G=101,I=0,J=0,K=0,B=H,100>=A,A>=1,B>=1] Inferred cost of f2(A,B,C,D,E): f2(A,B,C,D,E):[11]: 1 with precondition: [0>=B] f2(A,B,C,D,E):[12]: 2+it1*(1) Such that:it1=<100 with precondition: [B>=1] Solved cost expressions of f2(A,B,C,D,E): f2(A,B,C,D,E):[11]: 1 with precondition: [0>=B] f2(A,B,C,D,E):[12]: 102 with precondition: [B>=1] Maximum cost of f2(A,B,C,D,E): 102 Asymptotic class: constant Time statistics: Partial evaluation computed in 4 ms. Invariants computed in 12 ms. ----Backward Invariants 5 ms. ----Transitive Invariants 2 ms. Refinement performed in 10 ms. Termination proved in 5 ms. Upper bounds computed in 9 ms. ----Phase cost structures 2 ms. --------Equation cost structures 2 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 5 ms. ----Solving cost expressions 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 49 ms.