1 #define p (write_off - read_off >= 0)
2 #define q (write_off - read_off < HALF_UCHAR)
5 * Formula As Typed: [] (p && q)
6 * The Never Claim Below Corresponds
7 * To The Negated Formula !([] (p && q))
8 * (formalizing violations of the original)
11 never { /* !([] (p && q)) */
14 :: (((! ((p))) || (! ((q))))) -> goto accept_all
15 :: (1) -> goto T0_init
22 Use Load to open a file or a template.
25 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
26 (never claims generated from LTL formulae are stutter-invariant)
27 depth 0: Claim reached state 5 (line 321)
28 Running verification -- waiting for output
29 (kill background process 'pan' to abort run)
30 (use /bin/ps to find pid; then: kill -2 pid)