==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 61 state f28: 60+(-1*D) state f36: 54+(-8*D) state f39: (53+(-8*D))+(-1*E) state f50: 13+(-1*D) state f56: 0 state f60: 6+(-1*D) state ____f0: 62 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+39)+7)+1)+6)+1 \---