==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 139 state f67: 138+(-1*D) state f75: 132+(-21*D) state f78: (131+(-21*D))+(-1*E) state f89: 26+(-1*D) state f95: 0 state f99: 6+(-1*D) state ____f0: 140 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+104)+20)+1)+6)+1 \---