==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 203 state f4: 202+(-1*A) state f20: 201+(-1*B) state f31: 0 state ____f0: 204 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ (((1+101)+101)+1)+1 \---