==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 67 state f31: 66+(-1*D) state f39: 60+(-9*D) state f42: (59+(-9*D))+(-1*E) state f53: 14+(-1*D) state f59: 0 state f63: 6+(-1*D) state ____f0: 68 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+44)+8)+1)+6)+1 \---