==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 109 state f52: 108+(-1*D) state f60: 102+(-16*D) state f63: (101+(-16*D))+(-1*E) state f74: 21+(-1*D) state f80: 0 state f84: 6+(-1*D) state ____f0: 110 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+79)+15)+1)+6)+1 \---