==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 97 state f46: 96+(-1*D) state f54: 90+(-14*D) state f57: (89+(-14*D))+(-1*E) state f68: 19+(-1*D) state f74: 0 state f78: 6+(-1*D) state ____f0: 98 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+69)+13)+1)+6)+1 \---