NO


NON-Termination:
----------------
SCC:
+--transitions: t1,t13,t2,t3,t5,t6,t8
+--nodes: l0,l2,l3,l4,l7
Closed walk: 5 -> t8, t5, t3, t1, t13
deterministic: Forced for: X2, X7
Reachability checked!
- Recurrent Set Found:
{
	-1 + tmp___02_post == 0,
	-1 + tmp1_post == 0,
	Stored_post == 0,
	-1 + X11 == 0,
	-1 + X10 == 0,
	X9 == 0,
	-1 + X8 == 0,
	-1 + X7 == 0,
	X6 == 0,
	-1 + X5 == 0,
	tmp1_0 -X4 == 0,
	X3 == 0,
	-1 + X2 == 0,
	tmp1_0 -X1 == 0,
	X0 == 0,
	Stored_0 == 0
}
method 1