==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 103 state f49: 102+(-1*D) state f57: 96+(-15*D) state f60: (95+(-15*D))+(-1*E) state f71: 20+(-1*D) state f77: 0 state f81: 6+(-1*D) state ____f0: 104 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+74)+14)+1)+6)+1 \---