==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 73 state f34: 72+(-1*D) state f42: 66+(-10*D) state f45: (65+(-10*D))+(-1*E) state f56: 15+(-1*D) state f62: 0 state f66: 6+(-1*D) state ____f0: 74 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+49)+9)+1)+6)+1 \---