#define p	(write_off - read_off >= 0)
#define q	(write_off - read_off < HALF_UCHAR)

	/*
	 * Formula As Typed: [] (p && q)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([] (p && q))
	 * (formalizing violations of the original)
	 */

never {    /* !([] (p && q)) */
T0_init:
	if
	:: (((! ((p))) || (! ((q))))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

#ifdef NOTES
Use Load to open a file or a template.
#endif
#ifdef RESULT
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
depth 0: Claim reached state 5 (line 321)
Running verification -- waiting for output
	(kill background process 'pan' to abort run)
	(use /bin/ps to find pid; then: kill -2 pid)

#endif