==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 403 state f8: 402+(-2*A) state f14: 401+(-2*B) state f23: 201+(-2*A) state f28: 200+(-2*A) state f38: 0 state ____f0: 404 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ (((((1+101)+100)+101)+100)+1)+1 \---