never {    /* <>(c_forever_1 && c_forever_2) */
T0_init:
	if
	:: ((c_forever_1) && (c_forever_2)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}