warning: Ignored call to stop/4 in equation lbl41/4 Inferred cost of lbl41(A,B,C,D): lbl41(A,B,C,D):[7]: 1 with precondition: [D=C] Inferred cost of start(A,B,C,D): start(A,B,C,D):[9]: 2 with precondition: [B=A,D=C] Inferred cost of start0(A,B,C,D): start0(A,B,C,D):[11]: 3 with precondition: [] Solved cost expressions of start0(A,B,C,D): start0(A,B,C,D):[11]: 3 with precondition: [] Maximum cost of start0(A,B,C,D): 3 Asymptotic class: constant Time statistics: Partial evaluation computed in 1 ms. Invariants computed in 0 ms. ----Backward Invariants 0 ms. ----Transitive Invariants 0 ms. Refinement performed in 2 ms. Termination proved in 0 ms. Upper bounds computed in 3 ms. ----Phase cost structures 2 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 0 ms. Compressed phase information: 0 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 11 ms.