==> YES, main.fstb terminates. max_dim = 1 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state f0: 133 state f64: 132+(-1*D) state f72: 126+(-20*D) state f75: (125+(-20*D))+(-1*E) state f86: 25+(-1*D) state f92: 0 state f96: 6+(-1*D) state ____f0: 134 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | 1 >= 0 \ ((((((1+6)+6)+99)+19)+1)+6)+1 \---