==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 55 state f25: 54+(-1*D) state f33: 48+(-7*D) state f36: (47+(-7*D))+(-1*E) state f47: 12+(-1*D) state f53: 0 state f57: 6+(-1*D) state ____f0: 56 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+34)+6)+1)+6)+1 \---