WARNING: Excluded non-linear constraints:[C=A div B] warning: Ignored call to end/2 in equation (div)/2 warning: Ignored call to end/2 in equation (div)/2 warning: Ignored call to (-)/2 in equation (div)/2 Inferred cost of A div B: A div B:[7]: 1 with precondition: [0>=A] A div B:[8]: 1 with precondition: [A>=B] A div B:[9]: 1 with precondition: [A>=1,B>=A+1] Inferred cost of start(A,B): start(A,B):[11]: 2 with precondition: [0>=A] start(A,B):[12]: 2 with precondition: [A>=B] start(A,B):[13]: 2 with precondition: [A>=1,B>=A+1] Solved cost expressions of start(A,B): start(A,B):[11]: 2 with precondition: [0>=A] start(A,B):[12]: 2 with precondition: [A>=B] start(A,B):[13]: 2 with precondition: [A>=1,B>=A+1] Maximum cost of start(A,B): 2 Asymptotic class: constant Time statistics: Partial evaluation computed in 1 ms. Invariants computed in 1 ms. ----Backward Invariants 1 ms. ----Transitive Invariants 0 ms. Refinement performed in 3 ms. Termination proved in 0 ms. Upper bounds computed in 4 ms. ----Phase cost structures 1 ms. --------Equation cost structures 1 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 0 ms. ----Solving cost expressions 1 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 12 ms.