==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 121 state f58: 120+(-1*D) state f66: 114+(-18*D) state f69: (113+(-18*D))+(-1*E) state f80: 23+(-1*D) state f86: 0 state f90: 6+(-1*D) state ____f0: 122 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+89)+17)+1)+6)+1 \---