==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 85 state f40: 84+(-1*D) state f48: 78+(-12*D) state f51: (77+(-12*D))+(-1*E) state f62: 17+(-1*D) state f68: 0 state f72: 6+(-1*D) state ____f0: 86 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+59)+11)+1)+6)+1 \---