never {    /* ![]((c_start && <>c_exit) -> ((c_kfree -> ((c_kfree U c_exit) || (c_kfree U (!c_kfree U c_exit)))) U c_exit)) */
T0_init:
	if
	:: (! ((c_exit)) && (c_exit) && (c_kfree) && (c_start)) -> goto accept_S133
	:: (! ((c_exit)) && (c_start)) -> goto T0_S97
	:: (! ((c_exit)) && (c_kfree) && (c_start)) -> goto T0_S225
	:: (1) -> goto T0_init
	fi;
accept_S133:
	if
	:: (! ((c_exit))) -> goto T0_S133
	:: (! ((c_exit)) && ! ((c_kfree))) -> goto accept_S170
	fi;
accept_S170:
	if
	:: (! ((c_exit))) -> goto accept_S170
	:: (! ((c_exit)) && (c_kfree)) -> goto accept_all
	fi;
T0_S97:
	if
	:: (! ((c_exit))) -> goto T0_S97
	:: (! ((c_exit)) && (c_kfree)) -> goto T0_S225
	fi;
T0_S133:
	if
	:: (! ((c_exit))) -> goto accept_S133
	:: (! ((c_exit)) && ! ((c_kfree))) -> goto accept_S170
	fi;
T0_S225:
	if
	:: (! ((c_exit))) -> goto T0_S225
	:: (! ((c_exit)) && ! ((c_kfree))) -> goto T0_S251
	fi;
T0_S251:
	if
	:: (! ((c_exit))) -> goto T0_S251
	:: (! ((c_exit)) && (c_kfree)) -> goto T0_S2
	fi;
T0_S2:
	if
	:: ((c_exit)) -> goto accept_all
	:: (1) -> goto T0_S2
	fi;
accept_all:
	skip
}