/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume pesco/divbin_valuebound1.yml.witness.yml --witness.yaml.validate pesco/divbin_valuebound1.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/divbin_valuebound1.i


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Witness] CIL couldn't parse invariant: cond == (1) (../plain/divbin_valuebound1.i:23:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/divbin_valuebound1.i:23:5)
../plain/divbin_valuebound1.i:23: Error: Cannot resolve variable cond.
[Warning][Witness] couldn't locate invariant: (A >= (0U) && A <= (1U) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (3U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (7U)) || (A >= (0U) && A <= (1U) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && B >= (1U) && B <= (3U) && b == (B / (2U)) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && !(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U)))) && (!(b == (B / (2U))) || (b == (B / (2U)) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (7U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U))))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && (!(b == (B / (2U))) || (b == (B / (2U)) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (15U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U))))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (3U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && (!(b == (B / (2U))) || (b == (B / (2U)) && !(q == (1U)))) && !(q == (15U)) && !(q == (7U)) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (6U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && (!(b == (B / (2U))) || (b == (B / (2U)) && !(q == (1U)))) && !(q == (15U)) && !(q == (7U)) && !(q == (6U)) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (30U)) || (A >= (0U) && A <= (1U) && (!(b >= (1U)) || (b >= (1U) && !(b <= (16U))) || (b >= (1U) && b <= (16U) && !(q == (0U))) || (b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (1U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && !(q == (3U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U))))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (6U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (1U)) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b == (0U)) || (b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U)))) && (!(b == (0U)) || (b == (0U) && !(q == (6U)))) && B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && !(q == (3U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && !(q == (6U)) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (2U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (14U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && (!(b == (B / (2U))) || (b == (B / (2U)) && !(q == (1U)))) && !(q == (15U)) && !(q == (7U)) && !(q == (6U)) && !(q == (30U)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (14U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && !(q == (1U)) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (6U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (14U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (14U)))) && B >= (1U) && B <= (3U) && b == (B / (2U)) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(b >= (1U)) || (b >= (1U) && !(b <= (16U))) || (b >= (1U) && b <= (16U) && !(q == (0U))) || (b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (6U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U))))) && B >= (0U) && B <= (1U) && b == (0U) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && !(q == (3U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U)))) && !(q == (6U)) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U)))) && !(q == (14U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U))))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (0U) == B && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (6U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(q == (2U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U))) || (B >= (0U) && B <= (1U) && b == (0U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (2U)))) && !(B == (0U)) && b == (B / (2U)) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(b >= (1U)) || (b >= (1U) && !(b <= (16U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B)) && (!(b <= (1U)) || (b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(b <= (1U)) || (b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (6U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b <= (1U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (2U)))) && (!(b == (0U)) || (b == (0U) && !(q == (2U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (2U)))) && (B == (0U) || (!(B == (0U)) && !(b == (B / (2U))))) && B >= (0U) && B <= (1U) && b >= (0U) && b <= (8U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (16U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && !(q == (3U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && !(q == (15U)) && !(q == (7U)) && !(q == (6U)) && !(q == (30U)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U)))) && !(q == (14U)) && !(b == (B / (2U))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (2U)) || (A >= (0U) && A <= (1U) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (16U)))) && (!(b <= (1U)) || (b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U)))) && (!(b == (0U)) || (b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (6U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (30U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b <= (1U) && !(q == (2U)))) && (!(b == (0U)) || (b == (0U) && !(q == (6U)))) && (!(b <= (1U)) || (b <= (1U) && !(q == (2U)))) && (!(b == (0U)) || (b == (0U) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (14U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (2U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U))) || (B >= (0U) && B <= (1U) && b == (0U) && !(q == (2U)))) && (!(b == (0U)) || (b == (0U) && !(q == (2U)))) && (B == (0U) || (!(B == (0U)) && !(b == (B / (2U))))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b <= (8U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (2U)))) && B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1073741823U) && q == (0U) && r >= (0U) && r <= (1U)) (../plain/divbin_valuebound1.i:44:9)
[Warning][Witness] couldn't locate invariant: (A >= (0U) && A <= (1U) && B == (0U) && b == (0U) && q == (3U)) || (A >= (0U) && A <= (1U) && (!(B == (0U)) || (B == (0U) && !(b == (0U))) || (B == (0U) && b == (0U) && !(q == (3U)))) && B >= (2U) && B <= (2147483647U) && b >= (2U) && b <= (2147483647U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (2147483647U))) || (B >= (2U) && B <= (2147483647U) && !(b >= (2U))) || (B >= (2U) && B <= (2147483647U) && b >= (2U) && !(b <= (2147483647U)))) && !(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(B == (0U)) || (B == (0U) && !(b == (0U))) || (B == (0U) && b == (0U) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (2147483647U))) || (B >= (2U) && B <= (2147483647U) && !(b >= (2U))) || (B >= (2U) && B <= (2147483647U) && b >= (2U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (2147483647U) && b >= (2U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (2147483647U) && b >= (2U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (2147483647U) && b >= (2U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B) || (!(B == (0U)) && !((0U) == B) && !(q == (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && !(r >= (0U))) || (!(B == (0U)) && !((0U) == B) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (0U) && B <= (1U) && b == B && q == (1U)) (../plain/divbin_valuebound1.i:43:24)
[Info][Witness] unassume invariant: (((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && b == 2U * (2U * B)) || ((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && b == 2U * (2U * (2U * B)))) || (((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * (2U * (2U * B))))) || ((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * B)) || ((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((((((q == 0U && A >= 0U) && A <= 1U) && ((((! (r <= 1U) || (r <= 1U && ! (B >= 0U))) || ((r <= 1U && B >= 0U) && ! (B <= 1U))) || (((r <= 1U && B >= 0U) && B <= 1U) && ! (r >= 0U))) || (((((((((r <= 1U && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * B))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * (2U * B)))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && r >= 0U) && ! (r <= 1U)))) && b == B) && r == A)) && (((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && b == 2U * (2U * B)) || ((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && b == 2U * (2U * (2U * B)))) || (((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * (2U * (2U * B))))) || ((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * B)) || ((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((((((q == 0U && A >= 0U) && A <= 1U) && ((((! (r <= 1U) || (r <= 1U && ! (B >= 0U))) || ((r <= 1U && B >= 0U) && ! (B <= 1U))) || (((r <= 1U && B >= 0U) && B <= 1U) && ! (r >= 0U))) || (((((((((r <= 1U && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * B))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * (2U * B)))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && r >= 0U) && ! (r <= 1U)))) && b == B) && r == A)) (../plain/divbin_valuebound1.i:36:5-36:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin_valuebound1.i:39:9-39:18)
[Info][Witness] unassume invariant: (((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && b == 2U * (2U * B)) || ((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && b == 2U * (2U * (2U * B)))) || (((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * (2U * (2U * B))))) || ((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * B)) || ((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((((((q == 0U && A >= 0U) && A <= 1U) && ((((! (r <= 1U) || (r <= 1U && ! (B >= 0U))) || ((r <= 1U && B >= 0U) && ! (B <= 1U))) || (((r <= 1U && B >= 0U) && B <= 1U) && ! (r >= 0U))) || (((((((((r <= 1U && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * B))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * (2U * B)))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && r >= 0U) && ! (r <= 1U)))) && b == B) && r == A)) && (((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && b == 2U * (2U * B)) || ((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && b == 2U * (2U * (2U * B)))) || (((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * (2U * (2U * B))))) || ((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * B)) || ((((((((((((A >= 0U && A <= 1U) && q == 0U) && r <= 1U) && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((((((q == 0U && A >= 0U) && A <= 1U) && ((((! (r <= 1U) || (r <= 1U && ! (B >= 0U))) || ((r <= 1U && B >= 0U) && ! (B <= 1U))) || (((r <= 1U && B >= 0U) && B <= 1U) && ! (r >= 0U))) || (((((((((r <= 1U && B >= 0U) && B <= 1U) && r >= 0U) && ! (b == 2U * (2U * B))) && ! (b == 2U * (2U * (2U * B)))) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * B)) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * B))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * B))) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 2U * (2U * (2U * (2U * B)))))) || (((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && ! (r >= 0U))) || ((((B >= 0U && B <= 1U) && b == 2U * (2U * (2U * (2U * B)))) && r >= 0U) && ! (r <= 1U)))) && b == B) && r == A)) (../plain/divbin_valuebound1.i:39:9-39:18)
[Info][Witness] unassume invariant: (((((((B <= 1U && B >= 0U) && q == 0U) && r <= 1U) && r >= 0U) && A >= 0U) && A <= 1U) && ((((((b == 2U * B || (! (b == 2U * B) && b == 2U * (2U * (2U * (2U * B))))) || ((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && b == B)) || ((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * (2U * (2U * B)))) || ((((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * B)))) && ((((((((((((((((((((A >= 0U && A <= 1U) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 3U) || ((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 7U)) || (((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 15U)) || (((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 0U) && B <= 1U) && b >= 0U) && b <= 1U) && q == 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 31U)) || ((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && B >= 2U) && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 7U)) || (((((((((((((A >= 0U && A <= 1U) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && ! (q == 31U)) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || ((B >= 2U && B <= 4294967295U) && b == 0U))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 3U)) || (((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || ((B >= 1U && B <= 3U) && b == (B / 2U) / 2U))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 7U)) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 15U)) || (((((((((((((((A >= 0U && A <= 1U) && (! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 7U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b == 0U) && q == 3U)) || ((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == B / 2U) && q == 1U)) || ((((((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (B >= 0U) || (B >= 0U && ! (B <= 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 0U) || (b == 0U && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (! (b == 0U) || (b == 0U && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U)))) && B >= 2U) && B <= 4294967295U) && b >= 0U) && b <= 1U) && q == 1U)) || (((((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && r <= 1U) && q == 0U) && r >= 0U) && ! (B == 0U)) && ! (0U == B))) || ((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 32U)) || (((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && ! (b <= 32U)) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 64U)) (../plain/divbin_valuebound1.i:37:12-37:13)
[Info][Witness] unassume invariant: (((((((B <= 1U && B >= 0U) && q == 0U) && r <= 1U) && r >= 0U) && A >= 0U) && A <= 1U) && ((((((b == 2U * B || (! (b == 2U * B) && b == 2U * (2U * (2U * (2U * B))))) || ((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && b == B)) || ((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * (2U * (2U * B)))) || ((((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * B)))) && ((((((((((((((((((((A >= 0U && A <= 1U) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 3U) || ((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 7U)) || (((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 15U)) || (((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 0U) && B <= 1U) && b >= 0U) && b <= 1U) && q == 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 31U)) || ((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && B >= 2U) && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 7U)) || (((((((((((((A >= 0U && A <= 1U) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && ! (q == 31U)) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || ((B >= 2U && B <= 4294967295U) && b == 0U))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 3U)) || (((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || ((B >= 1U && B <= 3U) && b == (B / 2U) / 2U))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 7U)) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 15U)) || (((((((((((((((A >= 0U && A <= 1U) && (! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 7U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b == 0U) && q == 3U)) || ((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == B / 2U) && q == 1U)) || ((((((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (B >= 0U) || (B >= 0U && ! (B <= 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 0U) || (b == 0U && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (! (b == 0U) || (b == 0U && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U)))) && B >= 2U) && B <= 4294967295U) && b >= 0U) && b <= 1U) && q == 1U)) || (((((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && r <= 1U) && q == 0U) && r >= 0U) && ! (B == 0U)) && ! (0U == B))) || ((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 32U)) || (((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && ! (b <= 32U)) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 64U)) (../plain/divbin_valuebound1.i:38:13-38:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin_valuebound1.i:42:9-42:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin_valuebound1.i:44:9-44:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin_valuebound1.i:47:13-47:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/divbin_valuebound1.i:48:13-48:22)
[Info][Witness] unassume invariant: (((((((B <= 1U && B >= 0U) && q == 0U) && r <= 1U) && r >= 0U) && A >= 0U) && A <= 1U) && ((((((b == 2U * B || (! (b == 2U * B) && b == 2U * (2U * (2U * (2U * B))))) || ((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && b == B)) || ((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * (2U * (2U * B)))) || ((((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * B)))) && ((((((((((((((((((((A >= 0U && A <= 1U) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 3U) || ((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 7U)) || (((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 15U)) || (((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 0U) && B <= 1U) && b >= 0U) && b <= 1U) && q == 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 31U)) || ((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && B >= 2U) && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 7U)) || (((((((((((((A >= 0U && A <= 1U) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && ! (q == 31U)) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || ((B >= 2U && B <= 4294967295U) && b == 0U))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 3U)) || (((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || ((B >= 1U && B <= 3U) && b == (B / 2U) / 2U))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 7U)) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 15U)) || (((((((((((((((A >= 0U && A <= 1U) && (! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 7U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b == 0U) && q == 3U)) || ((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == B / 2U) && q == 1U)) || ((((((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (B >= 0U) || (B >= 0U && ! (B <= 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 0U) || (b == 0U && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (! (b == 0U) || (b == 0U && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U)))) && B >= 2U) && B <= 4294967295U) && b >= 0U) && b <= 1U) && q == 1U)) || (((((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && r <= 1U) && q == 0U) && r >= 0U) && ! (B == 0U)) && ! (0U == B))) || ((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 32U)) || (((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && ! (b <= 32U)) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 64U)) (../plain/divbin_valuebound1.i:48:13-48:22)
[Info][Witness] unassume invariant: (((((((B <= 1U && B >= 0U) && q == 0U) && r <= 1U) && r >= 0U) && A >= 0U) && A <= 1U) && ((((((b == 2U * B || (! (b == 2U * B) && b == 2U * (2U * (2U * (2U * B))))) || ((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) || (((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && b == B)) || ((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && b == 2U * (2U * (2U * (2U * (2U * B)))))) || (((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && b == 2U * (2U * (2U * B)))) || ((((((! (b == 2U * B) && ! (b == 2U * (2U * (2U * (2U * B))))) && ! (b == 2U * (2U * (2U * (2U * (2U * (2U * B))))))) && ! (b == B)) && ! (b == 2U * (2U * (2U * (2U * (2U * B)))))) && ! (b == 2U * (2U * (2U * B)))) && b == 2U * (2U * B)))) && ((((((((((((((((((((A >= 0U && A <= 1U) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 3U) || ((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 7U)) || (((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 15U)) || (((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 0U) && B <= 1U) && b >= 0U) && b <= 1U) && q == 1U)) || ((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 31U)) || ((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && B >= 2U) && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && r <= 1U)) || ((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 7U)) || (((((((((((((A >= 0U && A <= 1U) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U)))) && ! (q == 7U)) && ! (q == 15U)) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && ! (q == 31U)) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || ((B >= 2U && B <= 4294967295U) && b == 0U))) && B >= 1U) && B <= 3U) && b == (B / 2U) / 2U) && q == 3U)) || (((((((((((((A >= 0U && A <= 1U) && ! (q == 3U)) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || ((B >= 1U && B <= 3U) && b == (B / 2U) / 2U))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 7U)) && B >= 2U) && B <= 4294967295U) && b == 0U) && q == 15U)) || (((((((((((((((A >= 0U && A <= 1U) && (! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 8U))) || ((b >= 1U && b <= 8U) && ! (q == 0U))) || (((b >= 1U && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 7U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (q == 15U)))) && B >= 0U) && B <= 1U) && b == 0U) && q == 3U)) || ((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 31U)))) && ((((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U))) || ((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && ! (q == 0U))) || (((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 2U && B <= 4294967295U) && b >= 1U) && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (! (b == (B / 2U) / 2U) || (b == (B / 2U) / 2U && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && B >= 1U) && B <= 3U) && b == B / 2U) && q == 1U)) || ((((((((((((((((((A >= 0U && A <= 1U) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ((((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U))) || ((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && ! (q == 0U))) || (((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && ! (r >= 0U))) || ((((((B >= 0U && B <= 1U) && b >= 1U) && b <= 8U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (B >= 0U) || (B >= 0U && ! (B <= 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((((! (b >= 1U) || (b >= 1U && ! (b <= 2147483647U))) || ((b >= 1U && b <= 2147483647U) && ! (q == 0U))) || (((b >= 1U && b <= 2147483647U) && q == 0U) && ! (r >= 0U))) || ((((b >= 1U && b <= 2147483647U) && q == 0U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 0U) || (b == 0U && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (! (b == 0U) || (b == 0U && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && ((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U)))) && B >= 2U) && B <= 4294967295U) && b >= 0U) && b <= 1U) && q == 1U)) || (((((((((((((((((((A >= 0U && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 1U))) || (((B >= 0U && B <= 1U) && b >= 1U) && ! (b <= 8U)))) && ((((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b >= 0U))) || (((B >= 0U && B <= 1U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 0U && B <= 1U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 1U))) || (((B >= 2U && B <= 4294967295U) && b >= 1U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (((! (B >= 0U) || (B >= 0U && ! (B <= 1U))) || ((B >= 0U && B <= 1U) && ! (b == 0U))) || (((B >= 0U && B <= 1U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && r <= 1U) && q == 0U) && r >= 0U) && ! (B == 0U)) && ! (0U == B))) || ((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 32U)) || (((((((((((((((((((((((r <= 1U && q == 0U) && r >= 0U) && A >= 0U) && A <= 1U) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 15U)))) && ! (b <= 8U)) && ((! (b >= 0U) || (b >= 0U && ! (b <= 1U))) || ((b >= 0U && b <= 1U) && ! (q == 1U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 31U)))) && ((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b <= 2147483647U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 7U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == (B / 2U) / 2U))) || (((B >= 1U && B <= 3U) && b == (B / 2U) / 2U) && ! (q == 3U)))) && (((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b == 0U))) || (((B >= 2U && B <= 4294967295U) && b == 0U) && ! (q == 15U)))) && (! (b == 0U) || (b == 0U && ! (q == 3U)))) && (((! (B >= 1U) || (B >= 1U && ! (B <= 3U))) || ((B >= 1U && B <= 3U) && ! (b == B / 2U))) || (((B >= 1U && B <= 3U) && b == B / 2U) && ! (q == 1U)))) && ((((! (B >= 2U) || (B >= 2U && ! (B <= 4294967295U))) || ((B >= 2U && B <= 4294967295U) && ! (b >= 0U))) || (((B >= 2U && B <= 4294967295U) && b >= 0U) && ! (b <= 1U))) || ((((B >= 2U && B <= 4294967295U) && b >= 0U) && b <= 1U) && ! (q == 1U)))) && (B == 0U || (! (B == 0U) && 0U == B))) && ! (b <= 32U)) && B >= 0U) && B <= 1U) && b >= 1U) && b <= 64U)) (../plain/divbin_valuebound1.i:46:13-46:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin_valuebound1.i:51:5-51:38)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 32
  dead: 0
  total lines: 32
[Warning][Deadcode][CWE-571] condition 'B >= 0U' (possibly inserted by CIL) is always true (../plain/divbin_valuebound1.i:31:5-31:38)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/divbin_valuebound1.i:37:12-37:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/divbin_valuebound1.i:41:12-41:13)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/divbin_valuebound1.i:12:73-12:74)
[Warning][Deadcode][CWE-571] condition 'A >= 0U' (possibly inserted by CIL) is always true (../plain/divbin_valuebound1.i:29:5-29:38)
../plain/divbin_valuebound1.i:23: Error: Cannot resolve variable cond.

runtime: 00:00:10.132
vars: 79, evals: 139

|rho|=84
|called|=0
|stable|=84
|infl|=79
|wpoint|=1
|side_dep|=25
|side_infl|=49
|var_messages|=12
|rho_write|=33
|dep|=57
Found 8 contexts for 5 functions. Top 5 functions:
3	contexts for entry state of assume_abort_if_not (2023) on ../plain/divbin_valuebound1.i:15:1-17:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of reach_error (2015) on ../plain/divbin_valuebound1.i:12:1-12:160
1	contexts for entry state of main (2029) on ../plain/divbin_valuebound1.i:25:1-53:1
1	contexts for entry state of __VERIFIER_assert (2026) on ../plain/divbin_valuebound1.i:18:1-24:1

Memory statistics: total=1311.43MB, max=21.63MB, minor=1307.59MB, major=82.36MB, promoted=78.52MB
    minor collections=631  major collections=16 compactions=0

[Warning][Witness] invariant unconfirmed: (A >= (0U) && A <= (1U) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (3U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (7U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && !(q == (7U)) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (15U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (8U))) || (b >= (1U) && b <= (8U) && !(q == (0U))) || (b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && !(q == (7U)) && !(q == (15U)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (31U)) || (A >= (0U) && A <= (1U) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b <= (8U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && r <= (1U)) || (A >= (0U) && A <= (1U) && !(q == (3U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U))))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (7U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U)))) && !(q == (7U)) && !(q == (15U)) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && !(q == (31U)) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U))) && B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && q == (3U)) || (A >= (0U) && A <= (1U) && !(q == (3U)) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U))))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && !(q == (7U)) && B >= (2U) && B <= (4294967295U) && b == (0U) && q == (15U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (8U))) || (b >= (1U) && b <= (8U) && !(q == (0U))) || (b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U))))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(q == (15U)))) && B >= (0U) && B <= (1U) && b == (0U) && q == (3U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(b == ((B / (2U)) / (2U))) || (b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U))) || (B >= (0U) && B <= (1U) && b == (0U) && !(q == (3U)))) && B >= (1U) && B <= (3U) && b == (B / (2U)) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && !(q == (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b >= (1U) && b <= (8U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(b >= (1U)) || (b >= (1U) && !(b <= (2147483647U))) || (b >= (1U) && b <= (2147483647U) && !(q == (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && !(r >= (0U))) || (b >= (1U) && b <= (2147483647U) && q == (0U) && r >= (0U) && !(r <= (1U)))) && (!(b == (0U)) || (b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(b == (0U)) || (b == (0U) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U))) || (B >= (0U) && B <= (1U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U))))) && B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && q == (1U)) || (A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (1U))) || (B >= (0U) && B <= (1U) && b >= (1U) && !(b <= (8U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b >= (0U))) || (B >= (0U) && B <= (1U) && b >= (0U) && !(b <= (1U))) || (B >= (0U) && B <= (1U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (1U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (15U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == (0U))) || (B >= (0U) && B <= (1U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && r <= (1U) && q == (0U) && r >= (0U) && !(B == (0U)) && !((0U) == B)) || (r <= (1U) && q == (0U) && r >= (0U) && A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && !(b <= (8U)) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (15U)))) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B)) && B >= (0U) && B <= (1U) && b >= (1U) && b <= (32U)) || (r <= (1U) && q == (0U) && r >= (0U) && A >= (0U) && A <= (1U) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (15U)))) && !(b <= (8U)) && (!(b >= (0U)) || (b >= (0U) && !(b <= (1U))) || (b >= (0U) && b <= (1U) && !(q == (1U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (31U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b <= (2147483647U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (7U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == ((B / (2U)) / (2U)))) || (B >= (1U) && B <= (3U) && b == ((B / (2U)) / (2U)) && !(q == (3U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b == (0U))) || (B >= (2U) && B <= (4294967295U) && b == (0U) && !(q == (15U)))) && (!(b == (0U)) || (b == (0U) && !(q == (3U)))) && (!(B >= (1U)) || (B >= (1U) && !(B <= (3U))) || (B >= (1U) && B <= (3U) && !(b == (B / (2U)))) || (B >= (1U) && B <= (3U) && b == (B / (2U)) && !(q == (1U)))) && (!(B >= (2U)) || (B >= (2U) && !(B <= (4294967295U))) || (B >= (2U) && B <= (4294967295U) && !(b >= (0U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && !(b <= (1U))) || (B >= (2U) && B <= (4294967295U) && b >= (0U) && b <= (1U) && !(q == (1U)))) && (B == (0U) || (!(B == (0U)) && (0U) == B)) && !(b <= (32U)) && B >= (0U) && B <= (1U) && b >= (1U) && b <= (64U)) (../plain/divbin_valuebound1.i:38:24)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow
[Warning][Witness] invariant unconfirmed: B <= (1U) && B >= (0U) && q == (0U) && r <= (1U) && r >= (0U) && A >= (0U) && A <= (1U) && (b == ((2U) * B) || (!(b == ((2U) * B)) && b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) || (!(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) || (!(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) && b == B) || (!(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) && !(b == B) && b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) || (!(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) && !(b == B) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) && b == ((2U) * ((2U) * ((2U) * B)))) || (!(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) && !(b == B) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && b == ((2U) * ((2U) * B)))) (../plain/divbin_valuebound1.i:39:9)
[Warning][Witness] invariant unconfirmed: (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && b == ((2U) * ((2U) * B))) || (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && b == ((2U) * ((2U) * ((2U) * B)))) || (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) || (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) || (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) && b == ((2U) * B)) || (A >= (0U) && A <= (1U) && q == (0U) && r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) && !(b == ((2U) * B)) && b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))) || (q == (0U) && A >= (0U) && A <= (1U) && (!(r <= (1U)) || (r <= (1U) && !(B >= (0U))) || (r <= (1U) && B >= (0U) && !(B <= (1U))) || (r <= (1U) && B >= (0U) && B <= (1U) && !(r >= (0U))) || (r <= (1U) && B >= (0U) && B <= (1U) && r >= (0U) && !(b == ((2U) * ((2U) * B))) && !(b == ((2U) * ((2U) * ((2U) * B)))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B))))) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B)))))) && !(b == ((2U) * B)) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * ((2U) * B))))))))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == ((2U) * ((2U) * ((2U) * B))))) || (B >= (0U) && B <= (1U) && b == ((2U) * ((2U) * ((2U) * B))) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b == ((2U) * ((2U) * ((2U) * B))) && r >= (0U) && !(r <= (1U)))) && (!(B >= (0U)) || (B >= (0U) && !(B <= (1U))) || (B >= (0U) && B <= (1U) && !(b == ((2U) * ((2U) * ((2U) * ((2U) * B)))))) || (B >= (0U) && B <= (1U) && b == ((2U) * ((2U) * ((2U) * ((2U) * B)))) && !(r >= (0U))) || (B >= (0U) && B <= (1U) && b == ((2U) * ((2U) * ((2U) * ((2U) * B)))) && r >= (0U) && !(r <= (1U)))) && b == B && r == A) (../plain/divbin_valuebound1.i:37:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 4
  refuted: 0
  error: 3
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 7
SV-COMP result: unknown

vars = 79    evals = 139    narrow_reuses = 3

Timings:
                                  cputime   walltime   allocated   count
Default                           12.119s    12.120s   1379.61MB      1×
  preprocess                         0.030s     0.028s      0.01MB      1×
  FrontC                             0.006s     0.006s      4.18MB      4×
  Cabs2cil                           0.006s     0.006s      4.83MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                          12.070s    12.071s   1362.23MB      1×
    createCFG                          0.001s     0.001s      0.68MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.45MB     34×
        computeSCCs                        0.001s     0.001s      0.27MB     35×
    FrontC                             0.016s     0.016s     12.35MB     10×
    Cabs2cil                           0.011s     0.011s     11.09MB     10×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            8.563s     8.564s   1179.99MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    142×
      base unassume                      1.029s     1.029s   1009.43MB     28×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.081s     0.081s     29.07MB      1×
        postsolver_iter                    0.061s     0.061s     29.00MB      1×
    warn_global                        0.001s     0.001s      0.29MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
