==> YES, main.fstb terminates. max_dim = 2 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 13 state f10: (16+(-5*A))+B 2*C state f21: (16+(-5*A))+B 1+(2*C) state f32: 0 state ____f0: 14 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | H__o' >= 0 | 1 >= 0 \ (((1+-1)+-1)+1)+1 \---