never {    /* ![]((c_start && <>c_exit) -> ((c_alloc -> (!c_exit U c_free)) U c_exit)) */
T0_init:
	if
	:: (! ((c_exit)) && (c_start)) -> goto T0_S27
	:: (! ((c_exit)) && ! ((c_free)) && (c_alloc) && (c_start)) -> goto T0_S51
	:: (1) -> goto T0_init
	fi;
accept_S36:
	if
	:: (! ((c_free))) -> goto accept_S36
	:: (! ((c_free)) && (c_exit)) -> goto accept_all
	fi;
accept_S2:
	if
	:: ((c_exit)) -> goto accept_all
	:: (1) -> goto T0_S2
	fi;
T0_S27:
	if
	:: (! ((c_exit))) -> goto T0_S27
	:: (! ((c_exit)) && ! ((c_free)) && (c_alloc)) -> goto T0_S51
	fi;
T0_S51:
	if
	:: (! ((c_free)) && (c_exit)) -> goto accept_S36
	:: (! ((c_free)) && (c_exit)) -> goto accept_all
	:: (! ((c_free))) -> goto T0_S51
	:: (! ((c_free)) && (c_exit)) -> goto accept_S2
	fi;
T0_S2:
	if
	:: ((c_exit)) -> goto accept_all
	:: (1) -> goto T0_S2
	fi;
accept_all:
	skip
}