NO


NON-Termination:
----------------
SCC:
+--transitions: t4,t5
+--nodes: l5,l6
Closed walk: 2 -> t4, t5
deterministic: Forced for: X0, X1, X1, X0, X10, X9, X9, X10, X12, X12, X9, X9, X1, X1, X17, X17, X1, X1, X0, X1, X9, X10, X12, X17
Reachability checked!
- Recurrent Set Found:
{
	x_14_post == 0,
	x_134_post == 0,
	tp_33_0 -tp_33_post == 0,
	t_32_0 -t_32_post == 0,
	st_16_0 -st_16_post == 0,
	rv_31_0 -rv_31_post == 0,
	-2 + rv_13_post == 0,
	rt_11_0 -rt_11_post == 0,
	r_37_post == 0,
	r_135_post == 0,
	l_27_0 -l_27_post == 0,
	i_98_0 -i_98_post == 0,
	i_28_0 -i_28_post == 0,
	i_115_0 -i_115_post == 0,
	h_30_0 -h_30_post == 0,
	X3 -h_15_post == 0,
	-2 + a_76_post == 0,
	a_136_post == 0,
	a_123_post == 0,
	X18 == 0,
	X17 == 0,
	tp_33_0 -X16 == 0,
	t_32_0 -X15 == 0,
	st_16_0 -X14 == 0,
	rv_31_0 -X13 == 0,
	-2 + X12 == 0,
	rt_11_0 -X11 == 0,
	X10 == 0,
	X9 == 0,
	l_27_0 -X8 == 0,
	i_98_0 -X7 == 0,
	i_28_0 -X6 == 0,
	i_115_0 -X5 == 0,
	h_30_0 -X4 == 0,
	-2 + X2 == 0,
	X1 == 0,
	X0 == 0,
	x_14_0 == 0,
	-2 + rv_13_0 == 0,
	r_37_0 == 0,
	-2 + a_76_0 == 0,
	a_123_0 == 0,
	-2 + i_115_0 >= 0,
	-2 + i_28_0 >= 0
}
Connected Subgraphs where we couldn't prove Termination:
--------------------------------------------------------
SCC:
+--transitions: t7,t8
+--nodes: l4,l7


method 1