==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 79 state f37: 78+(-1*D) state f45: 72+(-11*D) state f48: (71+(-11*D))+(-1*E) state f59: 16+(-1*D) state f65: 0 state f69: 6+(-1*D) state ____f0: 80 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+54)+10)+1)+6)+1 \---