NO


NON-Termination:
----------------
SCC:
+--transitions: t14,t16
+--nodes: eval_main_bb10_in,eval_main_bb9_in
Closed walk: 2 -> t14, t16
Reachability checked!
- Recurrent Set Found:
{
	-1003 + v_m.0' == 0,
	v_l.0' == 0,
	-3 + v_k.0' == 0,
	v_j.0' == 0,
	v_i.0' == 0,
	-7 + v_8' == 0,
	-3 + v_7' == 0,
	v_6' == 0,
	-3 + v_4' == 0,
	v_3' == 0,
	v_19 -v_19' == 0,
	v_18 -v_18' == 0,
	v_17 -v_17' == 0,
	v_16 -v_16' == 0,
	-1003 + v_15' == 0,
	-1003 + v_13' == 0,
	-3 + v_12' == 0,
	-3 + v_11' == 0,
	v_10' == 0,
	-2 + v_1' == 0,
	-1003 + X19 == 0,
	X18 == 0,
	-3 + X17 == 0,
	X16 == 0,
	X15 == 0,
	-7 + X14 == 0,
	-3 + X13 == 0,
	X12 == 0,
	-3 + X11 == 0,
	X10 == 0,
	v_19 -X9 == 0,
	v_18 -X8 == 0,
	v_17 -X7 == 0,
	v_16 -X6 == 0,
	v_15 -X5 == 0,
	-1003 + X4 == 0,
	-3 + X3 == 0,
	-3 + X2 == 0,
	X1 == 0,
	-2 + X0 == 0,
	-1003 + v_m.0 == 0,
	v_l.0 == 0,
	-3 + v_k.0 == 0,
	v_j.0 == 0,
	v_i.0 == 0,
	-7 + v_8 == 0,
	-3 + v_7 == 0,
	v_6 == 0,
	-3 + v_4 == 0,
	v_3 == 0,
	-1003 + v_13 == 0,
	-3 + v_12 == 0,
	-3 + v_11 == 0,
	v_10 == 0,
	-2 + v_1 == 0
}
method 1