NO


NON-Termination:
----------------
SCC:
+--transitions: t10,t24,t8
+--nodes: l7,l8,l9
Closed walk: 3 -> t24, t10, t8
Reachability checked!
- Recurrent Set Found:
{
	-3 + y8_post == 0,
	3 + y16_0 -y16_post == 0,
	-4 + y12_post == 0,
	-3 + x7_post == 0,
	-3 + x15_post == 0,
	3 + x11_post == 0,
	tmp___1_0 -tmp___1_post == 0,
	-4 + tmp___0_post == 0,
	-3 + tmp_post == 0,
	ret_foo18_0 -ret_foo18_post == 0,
	-4 + ret_foo14_post == 0,
	-3 + ret_foo10_post == 0,
	k_0 -k_post == 0,
	-4 + j_post == 0,
	-3 + i_post == 0,
	i9_post == 0,
	i17_post == 0,
	i13_post == 0,
	-3 + X35 == 0,
	y16_0 -X34 == 0,
	-4 + X33 == 0,
	-3 + X32 == 0,
	-3 + X31 == 0,
	3 + X30 == 0,
	tmp___1_0 -X29 == 0,
	-4 + X28 == 0,
	-3 + X27 == 0,
	ret_foo18_0 -X26 == 0,
	-4 + X25 == 0,
	-3 + X24 == 0,
	k_0 -X23 == 0,
	-4 + X22 == 0,
	-3 + X21 == 0,
	X20 == 0,
	X19 == 0,
	X18 == 0,
	-3 + X17 == 0,
	y16_0 -X16 == 0,
	-4 + X15 == 0,
	-3 + X14 == 0,
	-3 + X13 == 0,
	3 + X12 == 0,
	tmp___1_0 -X11 == 0,
	-4 + X10 == 0,
	-3 + X9 == 0,
	ret_foo18_0 -X8 == 0,
	-4 + X7 == 0,
	-3 + X6 == 0,
	k_0 -X5 == 0,
	-4 + X4 == 0,
	-3 + X3 == 0,
	X2 == 0,
	X1 == 0,
	X0 == 0,
	-3 + y8_0 == 0,
	-4 + y12_0 == 0,
	-3 + x7_0 == 0,
	-3 + x15_0 == 0,
	3 + x11_0 == 0,
	-4 + tmp___0_0 == 0,
	-3 + tmp_0 == 0,
	-4 + ret_foo14_0 == 0,
	-3 + ret_foo10_0 == 0,
	-4 + j_0 == 0,
	-3 + i_0 == 0,
	i9_0 == 0,
	i17_0 == 0,
	i13_0 == 0,
	6 + y16_0 >= 0
}
method 1