==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 115 state f55: 114+(-1*D) state f63: 108+(-17*D) state f66: (107+(-17*D))+(-1*E) state f77: 22+(-1*D) state f83: 0 state f87: 6+(-1*D) state ____f0: 116 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+84)+16)+1)+6)+1 \---