/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/divbin2_valuebound1.yml.witness.yml --witness.yaml.validate pesco/divbin2_valuebound1.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/divbin2_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())) )
[Warning][Witness] couldn't locate invariant: (B == (1U) && A >= (2U) && A <= (3U) && b == (4U) && q == (0U) && r >= (2U) && r <= (3U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && r <= (15U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && r <= (7U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && A == (1U) && b == (2U) && q == (0U) && r == (1U)) || (B == (1U) && (!(b == (4U)) || (b == (4U) && !(q == (0U))) || (b == (4U) && q == (0U) && !(r >= (2U))) || (b == (4U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(q == (0U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(q == (0U))) || (A == (1U) && q == (0U) && !(r == (1U)))) && A >= (2U) && A <= (3U) && b == (2U) && q == (1U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (0U))) || (A >= (2U) && A <= (3U) && q == (0U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(b == (8U)) || (b == (8U) && !(q == (0U))) || (b == (8U) && q == (0U) && !(r >= (4U))) || (b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(q == (0U))) || (A == (1U) && b == (2U) && q == (0U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U)))) && A >= (4U) && A <= (7U) && b == (4U) && q == (1U)) || (B == (1U) && (!(b == (4U)) || (b == (4U) && !(q == (0U))) || (b == (4U) && q == (0U) && !(r >= (2U))) || (b == (4U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(q == (0U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(q == (0U))) || (A == (1U) && q == (0U) && !(r == (1U)))) && !(q == (1U)) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U))) && A >= (2U) && A <= (3U) && b == (2U) && q == (2U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (0U))) || (A >= (2U) && A <= (3U) && q == (0U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(b == (8U)) || (b == (8U) && !(q == (0U))) || (b == (8U) && q == (0U) && !(r >= (4U))) || (b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(q == (0U))) || (A == (1U) && b == (2U) && q == (0U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U))) && !(q == (1U)) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U)))) && A >= (4U) && A <= (7U) && b == (4U) && q == (2U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && !(b == (8U)) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U))) && !(q == (1U)) && !(q == (2U)) && A >= (4U) && A <= (7U) && b == (4U) && q == (0U) && r >= (4U) && r <= (7U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(b == (8U)) || (b == (8U) && !(q == (0U))) || (b == (8U) && q == (0U) && !(r >= (4U))) || (b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(q == (0U))) || (A == (1U) && q == (0U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U)))) && !(b == (4U)) && A >= (4U) && A <= (7U) && b == (2U) && q == (2U)) || (B == (1U) && (!(b == (4U)) || (b == (4U) && !(q == (0U))) || (b == (4U) && q == (0U) && !(r >= (2U))) || (b == (4U) && q == (0U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(q == (0U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && q == (0U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(q == (0U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && !(b == (2U)) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (0U))) || (A >= (4U) && A <= (7U) && b == (4U) && q == (0U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && q == (0U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U))) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && !(b == (2U)) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (2U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (2U)))) && A == (1U) && b == (1U) && q == (0U) && r == (1U)) || (B == (1U) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && !(b == (16U)) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (2U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (2U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U)))) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(r == (1U)))) && A >= (8U) && A <= (15U) && b == (8U) && q == (0U) && r >= (8U) && r <= (15U)) || (B == (1U) && !(b == (4U)) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && (!(A == (1U)) || (A == (1U) && !(r == (1U)))) && !(q == (1U)) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U))) && !(q == (2U)) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(r == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && r >= (8U) && !(r <= (15U)))) && A >= (2U) && A <= (3U) && b == (2U) && q == (0U) && r >= (2U) && r <= (3U)) (../plain/divbin2_valuebound1.i:41:9)
[Warning][Witness] couldn't locate invariant: (B == (1U) && A == (1U) && b == (1U) && q == (1U)) || (B == (1U) && b == (1U) && (!(A == (1U)) || (A == (1U) && !(q == (1U)))) && A == (0U) && q == (0U) && r == A) (../plain/divbin2_valuebound1.i:40:24)
[Error][Witness] CIL couldn't parse invariant: cond == (1) (../plain/divbin2_valuebound1.i:23:5)
[Info][Witness] invariant has undefined variables or side effects: cond == (1) (../plain/divbin2_valuebound1.i:23:5)
[Info][Witness] unassume invariant: (((((((((((B == 1U && q == 0U) && A >= 8U) && A <= 4294967295U) && b == 16U) && r == A) || (((((q == 0U && B == 1U) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U))) || (((A >= 8U && A <= 4294967295U) && b == 16U) && ! (r == A)))) && ! (A == 0U)) && b == 2U) && ! (0U == A))) || (((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && A >= 32U) && A <= 4294967295U) && b == 64U) && r == A)) || ((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && A >= 2U) && A <= 4294967295U) && b == 4U) && r == A)) || (((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && A >= 4U) && A <= 4294967295U) && b == 8U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && (! (A >= 4U) || (A >= 4U && ! (b == 8U)))) && A >= 16U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((((q == 0U && B == 1U) && ((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && ((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 64U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 4294967295U))) || ((A >= 2U && A <= 4294967295U) && ! (b == 4U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 8U)))) && ((! (A >= 16U) || (A >= 16U && ! (A <= 4294967295U))) || ((A >= 16U && A <= 4294967295U) && ! (b == 32U)))) && b == 1U) && r == A)) && (((((((((((B == 1U && q == 0U) && A >= 8U) && A <= 4294967295U) && b == 16U) && r == A) || (((((q == 0U && B == 1U) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U))) || (((A >= 8U && A <= 4294967295U) && b == 16U) && ! (r == A)))) && ! (A == 0U)) && b == 2U) && ! (0U == A))) || (((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && A >= 32U) && A <= 4294967295U) && b == 64U) && r == A)) || ((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && A >= 2U) && A <= 4294967295U) && b == 4U) && r == A)) || (((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && A >= 4U) && A <= 4294967295U) && b == 8U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && (! (A >= 4U) || (A >= 4U && ! (b == 8U)))) && A >= 16U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((((q == 0U && B == 1U) && ((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && ((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 64U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 4294967295U))) || ((A >= 2U && A <= 4294967295U) && ! (b == 4U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 8U)))) && ((! (A >= 16U) || (A >= 16U && ! (A <= 4294967295U))) || ((A >= 16U && A <= 4294967295U) && ! (b == 32U)))) && b == 1U) && r == A)) (../plain/divbin2_valuebound1.i:33:5-33:10)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin2_valuebound1.i:36:9-36:18)
[Info][Witness] unassume invariant: (((((((((((B == 1U && q == 0U) && A >= 8U) && A <= 4294967295U) && b == 16U) && r == A) || (((((q == 0U && B == 1U) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U))) || (((A >= 8U && A <= 4294967295U) && b == 16U) && ! (r == A)))) && ! (A == 0U)) && b == 2U) && ! (0U == A))) || (((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && A >= 32U) && A <= 4294967295U) && b == 64U) && r == A)) || ((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && A >= 2U) && A <= 4294967295U) && b == 4U) && r == A)) || (((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && A >= 4U) && A <= 4294967295U) && b == 8U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && (! (A >= 4U) || (A >= 4U && ! (b == 8U)))) && A >= 16U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((((q == 0U && B == 1U) && ((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && ((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 64U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 4294967295U))) || ((A >= 2U && A <= 4294967295U) && ! (b == 4U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 8U)))) && ((! (A >= 16U) || (A >= 16U && ! (A <= 4294967295U))) || ((A >= 16U && A <= 4294967295U) && ! (b == 32U)))) && b == 1U) && r == A)) && (((((((((((B == 1U && q == 0U) && A >= 8U) && A <= 4294967295U) && b == 16U) && r == A) || (((((q == 0U && B == 1U) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U))) || (((A >= 8U && A <= 4294967295U) && b == 16U) && ! (r == A)))) && ! (A == 0U)) && b == 2U) && ! (0U == A))) || (((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && A >= 32U) && A <= 4294967295U) && b == 64U) && r == A)) || ((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && A >= 2U) && A <= 4294967295U) && b == 4U) && r == A)) || (((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && A >= 4U) && A <= 4294967295U) && b == 8U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 8U) || (A >= 8U && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && (! (A >= 32U) || (A >= 32U && ! (b == 64U)))) && (! (A >= 2U) || (A >= 2U && ! (b == 4U)))) && (! (A >= 4U) || (A >= 4U && ! (b == 8U)))) && A >= 16U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((((q == 0U && B == 1U) && ((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 16U)))) && ((A == 0U || (! (A == 0U) && ! (b == 2U))) || ((! (A == 0U) && b == 2U) && 0U == A))) && ((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 64U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 4294967295U))) || ((A >= 2U && A <= 4294967295U) && ! (b == 4U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 8U)))) && ((! (A >= 16U) || (A >= 16U && ! (A <= 4294967295U))) || ((A >= 16U && A <= 4294967295U) && ! (b == 32U)))) && b == 1U) && r == A)) (../plain/divbin2_valuebound1.i:36:9-36:18)
[Info][Witness] unassume invariant: ((((((((((B == 1U && q == 0U) && A >= 4U) && A <= 4294967295U) && b == 4U) && r == A) || ((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && A >= 8U) && A <= 4294967295U) && b == 8U) && r == A)) || (((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && A >= 32U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((q == 0U && B == 1U) && (((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 4U))) || (((A >= 4U && A <= 4294967295U) && b == 4U) && ! (r == A)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 8U))) || (((A >= 8U && A <= 4294967295U) && b == 8U) && ! (r == A)))) && (((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 32U))) || (((A >= 32U && A <= 4294967295U) && b == 32U) && ! (r == A)))) && ! (A == 0U)) && b == 1U) && ! (0U == A))) || (((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && A >= 16U) && A <= 4294967295U) && b == 16U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && (! (A >= 16U) || (A >= 16U && ! (b == 16U)))) && A >= 2U) && A <= 4294967295U) && b == 2U) && r == A)) && (((((((((((((((B == 1U && A == 1U) && b == 1U) && q == 1U) || (((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && A >= 2U) && A <= 3U) && b == 2U) && q == 1U)) || ((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && A >= 8U) && A <= 15U) && b == 8U) && q == 1U)) || (((((((((B == 1U && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && A >= 4U) && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && r <= 1U)) || ((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && A >= 2U) && A <= 3U) && b == 1U) && q == 3U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && b == 2U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 3U)) && A >= 2U) && A <= 3U) && b == 1U) && q == 2U) && r == 0U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && A >= 4U) && A <= 7U) && b == 4U) && q == 1U)) || (((((((((((B == 1U && (! (b == 1U) || (b == 1U && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 2U))) || (((A >= 4U && A <= 7U) && q == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && q == 0U) && A == 1U) && b == 2U) && r == 1U)) || ((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 1U) || (b == 1U && ! (q == 3U)))) && ((! (b == 1U) || (b == 1U && ! (q == 2U))) || ((b == 1U && q == 2U) && ! (r == 0U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && A >= 2U) && A <= 3U) && b == 4U) && r >= 2U) && r <= 3U)) || (((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (q == 1U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (! (b == 4U) || (b == 4U && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && A >= 4U) && A <= 7U) && b == 8U) && r >= 4U) && r <= 7U)) || ((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (! (b == 8U) || (b == 8U && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && A >= 8U) && A <= 15U) && b == 16U) && r >= 8U) && r <= 15U)) || (((((((((((((((q == 0U && B == 1U) && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 3U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 2U))) || (((A >= 2U && A <= 3U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && A == 0U) && b == 1U) && r == A)) || ((((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && ((! (A == 0U) || (A == 0U && ! (b == 1U))) || ((A == 0U && b == 1U) && ! (r == A)))) && A >= 16U) && A <= 31U) && b == 32U) && r >= 16U) && r <= 31U)) (../plain/divbin2_valuebound1.i:34:12-34:13)
[Info][Witness] unassume invariant: ((((((((((B == 1U && q == 0U) && A >= 4U) && A <= 4294967295U) && b == 4U) && r == A) || ((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && A >= 8U) && A <= 4294967295U) && b == 8U) && r == A)) || (((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && A >= 32U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((q == 0U && B == 1U) && (((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 4U))) || (((A >= 4U && A <= 4294967295U) && b == 4U) && ! (r == A)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 8U))) || (((A >= 8U && A <= 4294967295U) && b == 8U) && ! (r == A)))) && (((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 32U))) || (((A >= 32U && A <= 4294967295U) && b == 32U) && ! (r == A)))) && ! (A == 0U)) && b == 1U) && ! (0U == A))) || (((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && A >= 16U) && A <= 4294967295U) && b == 16U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && (! (A >= 16U) || (A >= 16U && ! (b == 16U)))) && A >= 2U) && A <= 4294967295U) && b == 2U) && r == A)) && (((((((((((((((B == 1U && A == 1U) && b == 1U) && q == 1U) || (((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && A >= 2U) && A <= 3U) && b == 2U) && q == 1U)) || ((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && A >= 8U) && A <= 15U) && b == 8U) && q == 1U)) || (((((((((B == 1U && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && A >= 4U) && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && r <= 1U)) || ((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && A >= 2U) && A <= 3U) && b == 1U) && q == 3U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && b == 2U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 3U)) && A >= 2U) && A <= 3U) && b == 1U) && q == 2U) && r == 0U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && A >= 4U) && A <= 7U) && b == 4U) && q == 1U)) || (((((((((((B == 1U && (! (b == 1U) || (b == 1U && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 2U))) || (((A >= 4U && A <= 7U) && q == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && q == 0U) && A == 1U) && b == 2U) && r == 1U)) || ((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 1U) || (b == 1U && ! (q == 3U)))) && ((! (b == 1U) || (b == 1U && ! (q == 2U))) || ((b == 1U && q == 2U) && ! (r == 0U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && A >= 2U) && A <= 3U) && b == 4U) && r >= 2U) && r <= 3U)) || (((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (q == 1U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (! (b == 4U) || (b == 4U && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && A >= 4U) && A <= 7U) && b == 8U) && r >= 4U) && r <= 7U)) || ((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (! (b == 8U) || (b == 8U && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && A >= 8U) && A <= 15U) && b == 16U) && r >= 8U) && r <= 15U)) || (((((((((((((((q == 0U && B == 1U) && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 3U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 2U))) || (((A >= 2U && A <= 3U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && A == 0U) && b == 1U) && r == A)) || ((((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && ((! (A == 0U) || (A == 0U && ! (b == 1U))) || ((A == 0U && b == 1U) && ! (r == A)))) && A >= 16U) && A <= 31U) && b == 32U) && r >= 16U) && r <= 31U)) (../plain/divbin2_valuebound1.i:35:13-35:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin2_valuebound1.i:39:9-39:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin2_valuebound1.i:41:9-41:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin2_valuebound1.i:44:13-44:22)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/divbin2_valuebound1.i:45:13-45:22)
[Info][Witness] unassume invariant: ((((((((((B == 1U && q == 0U) && A >= 4U) && A <= 4294967295U) && b == 4U) && r == A) || ((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && A >= 8U) && A <= 4294967295U) && b == 8U) && r == A)) || (((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && A >= 32U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((q == 0U && B == 1U) && (((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 4U))) || (((A >= 4U && A <= 4294967295U) && b == 4U) && ! (r == A)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 8U))) || (((A >= 8U && A <= 4294967295U) && b == 8U) && ! (r == A)))) && (((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 32U))) || (((A >= 32U && A <= 4294967295U) && b == 32U) && ! (r == A)))) && ! (A == 0U)) && b == 1U) && ! (0U == A))) || (((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && A >= 16U) && A <= 4294967295U) && b == 16U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && (! (A >= 16U) || (A >= 16U && ! (b == 16U)))) && A >= 2U) && A <= 4294967295U) && b == 2U) && r == A)) && (((((((((((((((B == 1U && A == 1U) && b == 1U) && q == 1U) || (((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && A >= 2U) && A <= 3U) && b == 2U) && q == 1U)) || ((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && A >= 8U) && A <= 15U) && b == 8U) && q == 1U)) || (((((((((B == 1U && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && A >= 4U) && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && r <= 1U)) || ((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && A >= 2U) && A <= 3U) && b == 1U) && q == 3U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && b == 2U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 3U)) && A >= 2U) && A <= 3U) && b == 1U) && q == 2U) && r == 0U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && A >= 4U) && A <= 7U) && b == 4U) && q == 1U)) || (((((((((((B == 1U && (! (b == 1U) || (b == 1U && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 2U))) || (((A >= 4U && A <= 7U) && q == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && q == 0U) && A == 1U) && b == 2U) && r == 1U)) || ((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 1U) || (b == 1U && ! (q == 3U)))) && ((! (b == 1U) || (b == 1U && ! (q == 2U))) || ((b == 1U && q == 2U) && ! (r == 0U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && A >= 2U) && A <= 3U) && b == 4U) && r >= 2U) && r <= 3U)) || (((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (q == 1U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (! (b == 4U) || (b == 4U && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && A >= 4U) && A <= 7U) && b == 8U) && r >= 4U) && r <= 7U)) || ((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (! (b == 8U) || (b == 8U && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && A >= 8U) && A <= 15U) && b == 16U) && r >= 8U) && r <= 15U)) || (((((((((((((((q == 0U && B == 1U) && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 3U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 2U))) || (((A >= 2U && A <= 3U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && A == 0U) && b == 1U) && r == A)) || ((((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && ((! (A == 0U) || (A == 0U && ! (b == 1U))) || ((A == 0U && b == 1U) && ! (r == A)))) && A >= 16U) && A <= 31U) && b == 32U) && r >= 16U) && r <= 31U)) (../plain/divbin2_valuebound1.i:45:13-45:22)
[Info][Witness] unassume invariant: ((((((((((B == 1U && q == 0U) && A >= 4U) && A <= 4294967295U) && b == 4U) && r == A) || ((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && A >= 8U) && A <= 4294967295U) && b == 8U) && r == A)) || (((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && A >= 32U) && A <= 4294967295U) && b == 32U) && r == A)) || (((((((q == 0U && B == 1U) && (((! (A >= 4U) || (A >= 4U && ! (A <= 4294967295U))) || ((A >= 4U && A <= 4294967295U) && ! (b == 4U))) || (((A >= 4U && A <= 4294967295U) && b == 4U) && ! (r == A)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 4294967295U))) || ((A >= 8U && A <= 4294967295U) && ! (b == 8U))) || (((A >= 8U && A <= 4294967295U) && b == 8U) && ! (r == A)))) && (((! (A >= 32U) || (A >= 32U && ! (A <= 4294967295U))) || ((A >= 32U && A <= 4294967295U) && ! (b == 32U))) || (((A >= 32U && A <= 4294967295U) && b == 32U) && ! (r == A)))) && ! (A == 0U)) && b == 1U) && ! (0U == A))) || (((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && A >= 16U) && A <= 4294967295U) && b == 16U) && r == A)) || ((((((((((q == 0U && B == 1U) && (! (A >= 4U) || (A >= 4U && ! (b == 4U)))) && (! (A >= 8U) || (A >= 8U && ! (b == 8U)))) && (! (A >= 32U) || (A >= 32U && ! (b == 32U)))) && ((A == 0U || (! (A == 0U) && ! (b == 1U))) || ((! (A == 0U) && b == 1U) && 0U == A))) && (! (A >= 16U) || (A >= 16U && ! (b == 16U)))) && A >= 2U) && A <= 4294967295U) && b == 2U) && r == A)) && (((((((((((((((B == 1U && A == 1U) && b == 1U) && q == 1U) || (((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && A >= 2U) && A <= 3U) && b == 2U) && q == 1U)) || ((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && A >= 8U) && A <= 15U) && b == 8U) && q == 1U)) || (((((((((B == 1U && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && A >= 4U) && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && r <= 1U)) || ((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && A >= 2U) && A <= 3U) && b == 1U) && q == 3U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && b == 2U) && r >= 0U) && ! (r <= 1U)))) && ! (q == 3U)) && A >= 2U) && A <= 3U) && b == 1U) && q == 2U) && r == 0U)) || ((((((((((B == 1U && (! (A == 1U) || (A == 1U && ! (b == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && A >= 4U) && A <= 7U) && b == 4U) && q == 1U)) || (((((((((((B == 1U && (! (b == 1U) || (b == 1U && ! (q == 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 2U))) || (((A >= 4U && A <= 7U) && q == 2U) && ! (r >= 0U))) || ((((A >= 4U && A <= 7U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && q == 0U) && A == 1U) && b == 2U) && r == 1U)) || ((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (! (b == 2U) || (b == 2U && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (! (b == 1U) || (b == 1U && ! (q == 3U)))) && ((! (b == 1U) || (b == 1U && ! (q == 2U))) || ((b == 1U && q == 2U) && ! (r == 0U)))) && ((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && A >= 2U) && A <= 3U) && b == 4U) && r >= 2U) && r <= 3U)) || (((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && ((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (q == 1U)))) && (((! (b == 2U) || (b == 2U && ! (q == 2U))) || ((b == 2U && q == 2U) && ! (r >= 0U))) || (((b == 2U && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (! (b == 4U) || (b == 4U && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && A >= 4U) && A <= 7U) && b == 8U) && r >= 4U) && r <= 7U)) || ((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (! (b == 8U) || (b == 8U && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && A >= 8U) && A <= 15U) && b == 16U) && r >= 8U) && r <= 15U)) || (((((((((((((((q == 0U && B == 1U) && (! (A == 1U) || (A == 1U && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && ((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 3U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (q == 2U))) || (((A >= 2U && A <= 3U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && A == 0U) && b == 1U) && r == A)) || ((((((((((((((((((q == 0U && B == 1U) && ((! (A == 1U) || (A == 1U && ! (b == 1U))) || ((A == 1U && b == 1U) && ! (q == 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 2U))) || (((A >= 2U && A <= 3U) && b == 2U) && ! (q == 1U)))) && (((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 8U))) || (((A >= 8U && A <= 15U) && b == 8U) && ! (q == 1U)))) && (((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 2U))) || (((A >= 4U && A <= 7U) && b == 2U) && ! (q == 2U))) || ((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && ! (r >= 0U))) || (((((A >= 4U && A <= 7U) && b == 2U) && q == 2U) && r >= 0U) && ! (r <= 1U)))) && (((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 3U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 1U))) || (((A >= 2U && A <= 3U) && b == 1U) && ! (q == 2U))) || ((((A >= 2U && A <= 3U) && b == 1U) && q == 2U) && ! (r == 0U)))) && (((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 4U))) || (((A >= 4U && A <= 7U) && b == 4U) && ! (q == 1U)))) && ((! (A == 1U) || (A == 1U && ! (b == 2U))) || ((A == 1U && b == 2U) && ! (r == 1U)))) && ((((! (A >= 2U) || (A >= 2U && ! (A <= 3U))) || ((A >= 2U && A <= 3U) && ! (b == 4U))) || (((A >= 2U && A <= 3U) && b == 4U) && ! (r >= 2U))) || ((((A >= 2U && A <= 3U) && b == 4U) && r >= 2U) && ! (r <= 3U)))) && ((((! (A >= 4U) || (A >= 4U && ! (A <= 7U))) || ((A >= 4U && A <= 7U) && ! (b == 8U))) || (((A >= 4U && A <= 7U) && b == 8U) && ! (r >= 4U))) || ((((A >= 4U && A <= 7U) && b == 8U) && r >= 4U) && ! (r <= 7U)))) && ((((! (A >= 8U) || (A >= 8U && ! (A <= 15U))) || ((A >= 8U && A <= 15U) && ! (b == 16U))) || (((A >= 8U && A <= 15U) && b == 16U) && ! (r >= 8U))) || ((((A >= 8U && A <= 15U) && b == 16U) && r >= 8U) && ! (r <= 15U)))) && ((! (A == 0U) || (A == 0U && ! (b == 1U))) || ((A == 0U && b == 1U) && ! (r == A)))) && A >= 16U) && A <= 31U) && b == 32U) && r >= 16U) && r <= 31U)) (../plain/divbin2_valuebound1.i:43:13-43:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/divbin2_valuebound1.i:48:5-48:38)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 29
  dead: 0
  total lines: 29
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/divbin2_valuebound1.i:34:12-34:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/divbin2_valuebound1.i:38:12-38:13)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/divbin2_valuebound1.i:12:73-12:74)
[Warning][Deadcode][CWE-571] condition 'A >= 0U' (possibly inserted by CIL) is always true (../plain/divbin2_valuebound1.i:29:5-29:38)
../plain/divbin2_valuebound1.i:23: Error: Cannot resolve variable cond.
[Warning][Witness] invariant unconfirmed: (B == (1U) && q == (0U) && A >= (8U) && A <= (4294967295U) && b == (16U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(A <= (4294967295U))) || (A >= (8U) && A <= (4294967295U) && !(b == (16U))) || (A >= (8U) && A <= (4294967295U) && b == (16U) && !(r == A))) && !(A == (0U)) && b == (2U) && !((0U) == A)) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(b == (16U)))) && (A == (0U) || (!(A == (0U)) && !(b == (2U))) || (!(A == (0U)) && b == (2U) && (0U) == A)) && A >= (32U) && A <= (4294967295U) && b == (64U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(b == (16U)))) && (A == (0U) || (!(A == (0U)) && !(b == (2U))) || (!(A == (0U)) && b == (2U) && (0U) == A)) && (!(A >= (32U)) || (A >= (32U) && !(b == (64U)))) && A >= (2U) && A <= (4294967295U) && b == (4U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(b == (16U)))) && (A == (0U) || (!(A == (0U)) && !(b == (2U))) || (!(A == (0U)) && b == (2U) && (0U) == A)) && (!(A >= (32U)) || (A >= (32U) && !(b == (64U)))) && (!(A >= (2U)) || (A >= (2U) && !(b == (4U)))) && A >= (4U) && A <= (4294967295U) && b == (8U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(b == (16U)))) && (A == (0U) || (!(A == (0U)) && !(b == (2U))) || (!(A == (0U)) && b == (2U) && (0U) == A)) && (!(A >= (32U)) || (A >= (32U) && !(b == (64U)))) && (!(A >= (2U)) || (A >= (2U) && !(b == (4U)))) && (!(A >= (4U)) || (A >= (4U) && !(b == (8U)))) && A >= (16U) && A <= (4294967295U) && b == (32U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (8U)) || (A >= (8U) && !(A <= (4294967295U))) || (A >= (8U) && A <= (4294967295U) && !(b == (16U)))) && (A == (0U) || (!(A == (0U)) && !(b == (2U))) || (!(A == (0U)) && b == (2U) && (0U) == A)) && (!(A >= (32U)) || (A >= (32U) && !(A <= (4294967295U))) || (A >= (32U) && A <= (4294967295U) && !(b == (64U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (4294967295U))) || (A >= (2U) && A <= (4294967295U) && !(b == (4U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (4294967295U))) || (A >= (4U) && A <= (4294967295U) && !(b == (8U)))) && (!(A >= (16U)) || (A >= (16U) && !(A <= (4294967295U))) || (A >= (16U) && A <= (4294967295U) && !(b == (32U)))) && b == (1U) && r == A) (../plain/divbin2_valuebound1.i:34:5)
[Warning][Witness] invariant unconfirmed: (B == (1U) && A == (1U) && b == (1U) && q == (1U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U)))) && A >= (2U) && A <= (3U) && b == (2U) && q == (1U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U)))) && A >= (8U) && A <= (15U) && b == (8U) && q == (1U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && r <= (1U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(q == (1U)))) && (!(b == (2U)) || (b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && A >= (2U) && A <= (3U) && b == (1U) && q == (3U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(q == (1U)))) && (!(b == (2U)) || (b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && r >= (0U) && !(r <= (1U)))) && !(q == (3U)) && A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && r == (0U)) || (B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U)))) && (!(b == (2U)) || (b == (2U) && !(q == (2U))) || (b == (2U) && q == (2U) && !(r >= (0U))) || (b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && A >= (4U) && A <= (7U) && b == (4U) && q == (1U)) || (B == (1U) && (!(b == (1U)) || (b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && q == (0U) && A == (1U) && b == (2U) && r == (1U)) || (q == (0U) && B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(b == (2U)) || (b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(b == (1U)) || (b == (1U) && !(q == (3U)))) && (!(b == (1U)) || (b == (1U) && !(q == (2U))) || (b == (1U) && q == (2U) && !(r == (0U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(q == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && r <= (3U)) || (q == (0U) && B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(q == (1U)))) && (!(b == (2U)) || (b == (2U) && !(q == (2U))) || (b == (2U) && q == (2U) && !(r >= (0U))) || (b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(b == (4U)) || (b == (4U) && !(q == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && r <= (7U)) || (q == (0U) && B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (1U)))) && (!(b == (8U)) || (b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && r <= (15U)) || (q == (0U) && B == (1U) && (!(A == (1U)) || (A == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && q == (2U) && !(r == (0U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && A == (0U) && b == (1U) && r == A) || (q == (0U) && B == (1U) && (!(A == (1U)) || (A == (1U) && !(b == (1U))) || (A == (1U) && b == (1U) && !(q == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (2U))) || (A >= (2U) && A <= (3U) && b == (2U) && !(q == (1U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (8U))) || (A >= (8U) && A <= (15U) && b == (8U) && !(q == (1U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && !(q == (2U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && !(r >= (0U))) || (A >= (4U) && A <= (7U) && b == (2U) && q == (2U) && r >= (0U) && !(r <= (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (3U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (1U))) || (A >= (2U) && A <= (3U) && b == (1U) && !(q == (2U))) || (A >= (2U) && A <= (3U) && b == (1U) && q == (2U) && !(r == (0U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (4U))) || (A >= (4U) && A <= (7U) && b == (4U) && !(q == (1U)))) && (!(A == (1U)) || (A == (1U) && !(b == (2U))) || (A == (1U) && b == (2U) && !(r == (1U)))) && (!(A >= (2U)) || (A >= (2U) && !(A <= (3U))) || (A >= (2U) && A <= (3U) && !(b == (4U))) || (A >= (2U) && A <= (3U) && b == (4U) && !(r >= (2U))) || (A >= (2U) && A <= (3U) && b == (4U) && r >= (2U) && !(r <= (3U)))) && (!(A >= (4U)) || (A >= (4U) && !(A <= (7U))) || (A >= (4U) && A <= (7U) && !(b == (8U))) || (A >= (4U) && A <= (7U) && b == (8U) && !(r >= (4U))) || (A >= (4U) && A <= (7U) && b == (8U) && r >= (4U) && !(r <= (7U)))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (15U))) || (A >= (8U) && A <= (15U) && !(b == (16U))) || (A >= (8U) && A <= (15U) && b == (16U) && !(r >= (8U))) || (A >= (8U) && A <= (15U) && b == (16U) && r >= (8U) && !(r <= (15U)))) && (!(A == (0U)) || (A == (0U) && !(b == (1U))) || (A == (0U) && b == (1U) && !(r == A))) && A >= (16U) && A <= (31U) && b == (32U) && r >= (16U) && r <= (31U)) (../plain/divbin2_valuebound1.i:35:24)
[Warning][Witness] invariant unconfirmed: (B == (1U) && q == (0U) && A >= (4U) && A <= (4294967295U) && b == (4U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (4U)) || (A >= (4U) && !(b == (4U)))) && A >= (8U) && A <= (4294967295U) && b == (8U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (4U)) || (A >= (4U) && !(b == (4U)))) && (!(A >= (8U)) || (A >= (8U) && !(b == (8U)))) && A >= (32U) && A <= (4294967295U) && b == (32U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (4U)) || (A >= (4U) && !(A <= (4294967295U))) || (A >= (4U) && A <= (4294967295U) && !(b == (4U))) || (A >= (4U) && A <= (4294967295U) && b == (4U) && !(r == A))) && (!(A >= (8U)) || (A >= (8U) && !(A <= (4294967295U))) || (A >= (8U) && A <= (4294967295U) && !(b == (8U))) || (A >= (8U) && A <= (4294967295U) && b == (8U) && !(r == A))) && (!(A >= (32U)) || (A >= (32U) && !(A <= (4294967295U))) || (A >= (32U) && A <= (4294967295U) && !(b == (32U))) || (A >= (32U) && A <= (4294967295U) && b == (32U) && !(r == A))) && !(A == (0U)) && b == (1U) && !((0U) == A)) || (q == (0U) && B == (1U) && (!(A >= (4U)) || (A >= (4U) && !(b == (4U)))) && (!(A >= (8U)) || (A >= (8U) && !(b == (8U)))) && (!(A >= (32U)) || (A >= (32U) && !(b == (32U)))) && (A == (0U) || (!(A == (0U)) && !(b == (1U))) || (!(A == (0U)) && b == (1U) && (0U) == A)) && A >= (16U) && A <= (4294967295U) && b == (16U) && r == A) || (q == (0U) && B == (1U) && (!(A >= (4U)) || (A >= (4U) && !(b == (4U)))) && (!(A >= (8U)) || (A >= (8U) && !(b == (8U)))) && (!(A >= (32U)) || (A >= (32U) && !(b == (32U)))) && (A == (0U) || (!(A == (0U)) && !(b == (1U))) || (!(A == (0U)) && b == (1U) && (0U) == A)) && (!(A >= (16U)) || (A >= (16U) && !(b == (16U)))) && A >= (2U) && A <= (4294967295U) && b == (2U) && r == A) (../plain/divbin2_valuebound1.i:36:9)
[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 = 56    evals = 118    narrow_reuses = 3

Timings:
../plain/divbin2_valuebound1.i:23: Error: Cannot resolve variable cond.
                                  cputime   walltime   allocated   count
Default                            8.071s     8.217s    922.96MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.17MB      4×
  Cabs2cil                           0.006s     0.006s      4.80MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                           8.031s     8.177s    905.65MB      1×
    createCFG                          0.001s     0.001s      0.65MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.43MB     34×
        computeSCCs                        0.001s     0.001s      0.25MB     35×
    FrontC                             0.023s     0.023s      8.14MB     10×
    Cabs2cil                           0.007s     0.007s      7.16MB     10×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            5.727s     5.863s    778.94MB      1×
      S.Dom.equal                        0.001s     0.001s      0.05MB    121×
      base unassume                      0.736s     0.736s    653.47MB     30×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.031s     0.031s     19.82MB      1×
        postsolver_iter                    0.031s     0.031s     19.77MB      1×
    warn_global                        0.001s     0.001s      0.24MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
