==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 145 state f70: 144+(-1*D) state f78: 138+(-22*D) state f81: (137+(-22*D))+(-1*E) state f92: 27+(-1*D) state f98: 0 state f102: 6+(-1*D) state ____f0: 146 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+109)+21)+1)+6)+1 \---