/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/cohendiv-ll_unwindbound2.yml.witness.yml --witness.yaml.validate pesco/cohendiv-ll_unwindbound2.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/cohendiv-ll_unwindbound2.c


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


--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: (x >= (1) && x <= (2147483647) && q == (0LL) && y >= (1) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && r <= (2147483647LL) && y <= (2147483647)) || (r <= (2147483647LL) && x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && y <= (1073741823)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (((!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL))) && !(r <= (2147483647LL))) || (r <= (2147483647LL) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && !(r >= (2LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && r <= (2147483645LL) && y <= (1073741823)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (!(r <= (2147483647LL)) || (r <= (2147483647LL) && !(r >= (1LL)) && !(counter == (3))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && !(a == (2LL))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(r >= (2LL))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && !(y <= (1073741823)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(r >= (-2147483644LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (-2147483646LL) && r <= (2147483646LL) && y <= (2147483647)) (../plain/cohendiv-ll_unwindbound2.c:52:3)
[Warning][Witness] couldn't locate invariant: x >= (1) && x <= (2147483647) && q == (0LL) && y >= (1) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && r <= (2147483647LL) && y <= (2147483647) (../plain/cohendiv-ll_unwindbound2.c:47:6)
[Warning][Witness] couldn't locate invariant: (y >= (1) && counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && x >= (1) && x <= (2147483647) && y <= (2147483647)) || (y >= (1) && (!(counter == (3)) || (counter == (3) && !(a == (1LL))) || (counter == (3) && a == (1LL) && !(b == ((long long int)y))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(x >= (1))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && x >= (1) && !(x <= (2147483647)))) && counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && !(x == (2147483647)) && y <= (2147483647)) || (y >= (1) && (!(counter == (3)) || (counter == (3) && !(a == (1LL))) || (counter == (3) && a == (1LL) && !(b == ((long long int)y))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && !(y <= (2147483647)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(b == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && !(r >= (-2147483648LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && !(r <= (2147483646LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && x == (2147483647)) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && !(x == (2147483647)) && !(y <= (2147483647)))) && counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && x >= (1) && x <= (2147483647) && y <= (1073741823)) (../plain/cohendiv-ll_unwindbound2.c:63:5)
[Warning][Witness] couldn't locate invariant: (x >= (1) && x <= (2147483647) && q == (0LL) && y >= (1) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && r <= (2147483647LL) && y <= (2147483647)) || (r <= (2147483647LL) && x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && y <= (1073741823)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (((!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL))) && !(r <= (2147483647LL))) || (r <= (2147483647LL) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && !(r >= (2LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && r <= (2147483645LL) && y <= (1073741823)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && (!(r <= (2147483647LL)) || (r <= (2147483647LL) && !(r >= (1LL)) && !(counter == (3))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && !(a == (2LL))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(r >= (2LL))) || (r <= (2147483647LL) && !(r >= (1LL)) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && !(y <= (1073741823)))) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(r >= (-2147483644LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (-2147483646LL) && r <= (2147483646LL) && y <= (2147483647)) (../plain/cohendiv-ll_unwindbound2.c:59:2)
[Info][Witness] unassume invariant: (((((((((((((y >= 1 && x >= 1) && x <= 2147483647) && counter == 2) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && y <= 2147483647) || ((((((((((x >= 1 && y >= 1) && x <= 2147483647) && ((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && y <= 1073741823)) || (((((((y >= 1 && ((((((((! (x >= 1) || (x >= 1 && ! (x <= 2147483647))) || (((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && ! (counter == 3))) || ((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && ! (a == 2LL))) || (((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && ! (b == 2LL * (long long )y))) || ((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || (((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && counter == 0) && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y <= 2147483647)) || ((((((((((y >= 1 && ((((((((! (x >= 1) || (x >= 1 && ! (x <= 2147483647))) || (((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && ! (counter == 3))) || ((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && ! (a == 2LL))) || (((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && ! (b == 2LL * (long long )y))) || ((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || (((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && ! (counter == 0)) && ((((((((! (counter == 3) || (counter == 3 && ! (a == 2LL))) || ((counter == 3 && a == 2LL) && ! (b == 2LL * (long long )y))) || (((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || ((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || (((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || ((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (x >= 1))) || (((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && ! (x <= 2147483647))) || ((((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && ! (y <= 1073741823)))) && (((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (x >= 1))) || (((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && ! (x <= 2147483647)))) && counter == 1) && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y <= 2147483647)) || (((((((((((((y >= 1 && ((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && (((((! (counter == 0) || (counter == 0 && ! (a == 0LL))) || ((counter == 0 && a == 0LL) && ! (b == 0LL))) || (((counter == 0 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x))) || (((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && ! (y <= 2147483647)))) && ! (counter == 3)) && (((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x))) || (((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && ! (y <= 2147483647)))) && counter == 4) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && y <= 1073741823)) || ((((((((((((((y >= 1 && ! (counter == 2)) && ((((! (counter == 0) || (counter == 0 && ! (a == 0LL))) || ((counter == 0 && a == 0LL) && ! (b == 0LL))) || (((counter == 0 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x)))) && (((((! (a == 2LL) || (a == 2LL && ! (b == 2LL * (long long )y))) || ((a == 2LL && b == 2LL * (long long )y) && ! (q == 2LL))) || (((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && ((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x)))) && ((((((! (counter == 4) || (counter == 4 && ! (a == 2LL))) || ((counter == 4 && a == 2LL) && ! (b == 2LL * (long long )y))) || (((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || ((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || (((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || ((((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && counter == 3) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && x <= 2147483647) && y <= 2147483647) (../plain/cohendiv-ll_unwindbound2.c:35:5-35:10)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:51:10-51:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:54:6-54:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/cohendiv-ll_unwindbound2.c:56:6-56:15)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:57:6-57:15)
[Info][Witness] unassume invariant: (((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y >= 1) && y <= 2147483647) && ((((((((((((x >= 1 && x <= 2147483647) && q == 0LL) && y >= 1) && r <= 2147483647LL) && counter == 1) && a == 1LL) && b == (long long )y) && r >= 1LL) && y <= 2147483647) || ((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ((((! (counter == 1) || (counter == 1 && ! (a == 1LL))) || ((counter == 1 && a == 1LL) && ! (b == (long long )y))) || (((counter == 1 && a == 1LL) && b == (long long )y) && ! (r >= 1LL))) || ((((counter == 1 && a == 1LL) && b == (long long )y) && r >= 1LL) && ! (y <= 2147483647)))) && counter == 2) && a == 2LL) && b == 2LL * (long long )y) && r >= 2LL) && y <= 1073741823)) || (((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ! (counter == 1)) && (((! (a == 2LL) || (a == 2LL && ! (b == 2LL * (long long )y))) || ((a == 2LL && b == 2LL * (long long )y) && ! (r >= 2LL))) || (((a == 2LL && b == 2LL * (long long )y) && r >= 2LL) && ! (y <= 1073741823)))) && counter == 2) && a == 1LL) && b == (long long )y) && r >= 1LL) && y <= 2147483647)) || (((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ((((! (counter == 1) || (counter == 1 && ! (a == 1LL))) || ((counter == 1 && a == 1LL) && ! (b == (long long )y))) || (((counter == 1 && a == 1LL) && b == (long long )y) && ! (r >= 1LL))) || ((((counter == 1 && a == 1LL) && b == (long long )y) && r >= 1LL) && ! (y <= 2147483647)))) && ! (counter == 2)) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && r >= 2LL) && y <= 1073741823))) && (((((((((((y >= 1 && counter == 3) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && x <= 2147483647) && y <= 2147483647) || (((((((((y >= 1 && ((((((! (counter == 3) || (counter == 3 && ! (a == 1LL))) || ((counter == 3 && a == 1LL) && ! (b == (long long )y))) || (((counter == 3 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (x >= 1))) || ((((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && x >= 1) && ! (x <= 2147483647)))) && counter == 1) && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && ! (x == 2147483647)) && y <= 2147483647)) || (((((((((((y >= 1 && ((((((! (counter == 3) || (counter == 3 && ! (a == 1LL))) || ((counter == 3 && a == 1LL) && ! (b == (long long )y))) || (((counter == 3 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && (((((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r >= (-0x7FFFFFFF-1)))) || (((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && ! (r <= 2147483646LL))) || ((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && x == 2147483647)) || (((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && ! (x == 2147483647)) && ! (y <= 2147483647)))) && counter == 4) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && y <= 1073741823)) (../plain/cohendiv-ll_unwindbound2.c:57:6-57:15)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:38:2-38:29)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:39:2-39:33)
[Info][Witness] unassume invariant: (((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y >= 1) && y <= 2147483647) && ((((((((((((x >= 1 && x <= 2147483647) && q == 0LL) && y >= 1) && r <= 2147483647LL) && counter == 1) && a == 1LL) && b == (long long )y) && r >= 1LL) && y <= 2147483647) || ((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ((((! (counter == 1) || (counter == 1 && ! (a == 1LL))) || ((counter == 1 && a == 1LL) && ! (b == (long long )y))) || (((counter == 1 && a == 1LL) && b == (long long )y) && ! (r >= 1LL))) || ((((counter == 1 && a == 1LL) && b == (long long )y) && r >= 1LL) && ! (y <= 2147483647)))) && counter == 2) && a == 2LL) && b == 2LL * (long long )y) && r >= 2LL) && y <= 1073741823)) || (((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ! (counter == 1)) && (((! (a == 2LL) || (a == 2LL && ! (b == 2LL * (long long )y))) || ((a == 2LL && b == 2LL * (long long )y) && ! (r >= 2LL))) || (((a == 2LL && b == 2LL * (long long )y) && r >= 2LL) && ! (y <= 1073741823)))) && counter == 2) && a == 1LL) && b == (long long )y) && r >= 1LL) && y <= 2147483647)) || (((((((((((x >= 1 && y >= 1) && x <= 2147483647) && q == 0LL) && r <= 2147483647LL) && ((((! (counter == 1) || (counter == 1 && ! (a == 1LL))) || ((counter == 1 && a == 1LL) && ! (b == (long long )y))) || (((counter == 1 && a == 1LL) && b == (long long )y) && ! (r >= 1LL))) || ((((counter == 1 && a == 1LL) && b == (long long )y) && r >= 1LL) && ! (y <= 2147483647)))) && ! (counter == 2)) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && r >= 2LL) && y <= 1073741823))) && (((((((((((y >= 1 && counter == 3) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && x <= 2147483647) && y <= 2147483647) || (((((((((y >= 1 && ((((((! (counter == 3) || (counter == 3 && ! (a == 1LL))) || ((counter == 3 && a == 1LL) && ! (b == (long long )y))) || (((counter == 3 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (x >= 1))) || ((((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && x >= 1) && ! (x <= 2147483647)))) && counter == 1) && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && ! (x == 2147483647)) && y <= 2147483647)) || (((((((((((y >= 1 && ((((((! (counter == 3) || (counter == 3 && ! (a == 1LL))) || ((counter == 3 && a == 1LL) && ! (b == (long long )y))) || (((counter == 3 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 3 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && (((((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r >= (-0x7FFFFFFF-1)))) || (((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && ! (r <= 2147483646LL))) || ((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && x == 2147483647)) || (((((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r >= (-0x7FFFFFFF-1)) && r <= 2147483646LL) && ! (x == 2147483647)) && ! (y <= 2147483647)))) && counter == 4) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && y <= 1073741823)) (../plain/cohendiv-ll_unwindbound2.c:44:2-44:7)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:47:6-47:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:48:6-48:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:59:2-59:11)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/cohendiv-ll_unwindbound2.c:60:2-60:11)
[Info][Witness] unassume invariant: (((((((((((((y >= 1 && x >= 1) && x <= 2147483647) && counter == 2) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && y <= 2147483647) || ((((((((((x >= 1 && y >= 1) && x <= 2147483647) && ((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && y <= 1073741823)) || (((((((y >= 1 && ((((((((! (x >= 1) || (x >= 1 && ! (x <= 2147483647))) || (((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && ! (counter == 3))) || ((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && ! (a == 2LL))) || (((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && ! (b == 2LL * (long long )y))) || ((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || (((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && counter == 0) && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y <= 2147483647)) || ((((((((((y >= 1 && ((((((((! (x >= 1) || (x >= 1 && ! (x <= 2147483647))) || (((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && ! (counter == 3))) || ((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && ! (a == 2LL))) || (((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && ! (b == 2LL * (long long )y))) || ((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || (((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((((((x >= 1 && x <= 2147483647) && (((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL)))) && counter == 3) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && ! (counter == 0)) && ((((((((! (counter == 3) || (counter == 3 && ! (a == 2LL))) || ((counter == 3 && a == 2LL) && ! (b == 2LL * (long long )y))) || (((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || ((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || (((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || ((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (x >= 1))) || (((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && ! (x <= 2147483647))) || ((((((((counter == 3 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && ! (y <= 1073741823)))) && (((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (x >= 1))) || (((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && ! (x <= 2147483647)))) && counter == 1) && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && y <= 2147483647)) || (((((((((((((y >= 1 && ((((((! (counter == 2) || (counter == 2 && ! (a == 1LL))) || ((counter == 2 && a == 1LL) && ! (b == (long long )y))) || (((counter == 2 && a == 1LL) && b == (long long )y) && ! (q == 1LL))) || ((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && ! (r >= -2147483646LL))) || (((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && ! (r <= 2147483646LL))) || ((((((counter == 2 && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && ! (y <= 2147483647)))) && (((((! (counter == 0) || (counter == 0 && ! (a == 0LL))) || ((counter == 0 && a == 0LL) && ! (b == 0LL))) || (((counter == 0 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x))) || (((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && ! (y <= 2147483647)))) && ! (counter == 3)) && (((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x))) || (((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && r == (long long )x) && ! (y <= 2147483647)))) && counter == 4) && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && x >= 1) && x <= 2147483647) && y <= 1073741823)) || ((((((((((((((y >= 1 && ! (counter == 2)) && ((((! (counter == 0) || (counter == 0 && ! (a == 0LL))) || ((counter == 0 && a == 0LL) && ! (b == 0LL))) || (((counter == 0 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 0 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x)))) && (((((! (a == 2LL) || (a == 2LL && ! (b == 2LL * (long long )y))) || ((a == 2LL && b == 2LL * (long long )y) && ! (q == 2LL))) || (((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || ((((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || (((((a == 2LL && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && ((((! (counter == 1) || (counter == 1 && ! (a == 0LL))) || ((counter == 1 && a == 0LL) && ! (b == 0LL))) || (((counter == 1 && a == 0LL) && b == 0LL) && ! (q == 0LL))) || ((((counter == 1 && a == 0LL) && b == 0LL) && q == 0LL) && ! (r == (long long )x)))) && ((((((! (counter == 4) || (counter == 4 && ! (a == 2LL))) || ((counter == 4 && a == 2LL) && ! (b == 2LL * (long long )y))) || (((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && ! (q == 2LL))) || ((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && ! (r >= -2147483644LL))) || (((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && ! (r <= 2147483645LL))) || ((((((counter == 4 && a == 2LL) && b == 2LL * (long long )y) && q == 2LL) && r >= -2147483644LL) && r <= 2147483645LL) && ! (y <= 1073741823)))) && counter == 3) && a == 1LL) && b == (long long )y) && q == 1LL) && r >= -2147483646LL) && r <= 2147483646LL) && x >= 1) && x <= 2147483647) && y <= 2147483647) (../plain/cohendiv-ll_unwindbound2.c:60:2-60:11)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/cohendiv-ll_unwindbound2.c:63:5-63:36)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 35
  dead: 0
  total lines: 35
[Error][Witness] invariant refuted: (y >= (1) && counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && x >= (1) && x <= (2147483647) && y <= (2147483647)) || (y >= (1) && (!(counter == (3)) || (counter == (3) && !(a == (1LL))) || (counter == (3) && a == (1LL) && !(b == ((long long int)y))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(x >= (1))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && x >= (1) && !(x <= (2147483647)))) && counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && !(x == (2147483647)) && y <= (2147483647)) || (y >= (1) && (!(counter == (3)) || (counter == (3) && !(a == (1LL))) || (counter == (3) && a == (1LL) && !(b == ((long long int)y))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL))) || (counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && !(y <= (2147483647)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(b == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && !(r >= (-2147483648LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && !(r <= (2147483646LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && x == (2147483647)) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r >= (-2147483648LL) && r <= (2147483646LL) && !(x == (2147483647)) && !(y <= (2147483647)))) && counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && x >= (1) && x <= (2147483647) && y <= (1073741823)) (../plain/cohendiv-ll_unwindbound2.c:42:6)
[Warning][Witness] invariant unconfirmed: (x >= (1) && x <= (2147483647) && q == (0LL) && y >= (1) && r <= (2147483647LL) && counter == (1) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && y <= (2147483647)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && r <= (2147483647LL) && (!(counter == (1)) || (counter == (1) && !(a == (1LL))) || (counter == (1) && a == (1LL) && !(b == ((long long int)y))) || (counter == (1) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (1) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && counter == (2) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && y <= (1073741823)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && r <= (2147483647LL) && !(counter == (1)) && (!(a == (2LL)) || (a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && !(r >= (2LL))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && !(y <= (1073741823)))) && counter == (2) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && y <= (2147483647)) || (x >= (1) && y >= (1) && x <= (2147483647) && q == (0LL) && r <= (2147483647LL) && (!(counter == (1)) || (counter == (1) && !(a == (1LL))) || (counter == (1) && a == (1LL) && !(b == ((long long int)y))) || (counter == (1) && a == (1LL) && b == ((long long int)y) && !(r >= (1LL))) || (counter == (1) && a == (1LL) && b == ((long long int)y) && r >= (1LL) && !(y <= (2147483647)))) && !(counter == (2)) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && r >= (2LL) && y <= (1073741823)) (../plain/cohendiv-ll_unwindbound2.c:46:2)
[Error][Witness] invariant refuted: counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r == ((long long int)x) && y >= (1) && y <= (2147483647) (../plain/cohendiv-ll_unwindbound2.c:38:2)
[Warning][Witness] invariant unconfirmed: (y >= (1) && x >= (1) && x <= (2147483647) && counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && y <= (2147483647)) || (x >= (1) && y >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && !(y <= (2147483647)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && y <= (1073741823)) || (y >= (1) && (!(x >= (1)) || (x >= (1) && !(x <= (2147483647))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && !(counter == (3))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && !(a == (2LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(q == (2LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && !(r >= (-2147483644LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && counter == (0) && a == (0LL) && b == (0LL) && q == (0LL) && r == ((long long int)x) && y <= (2147483647)) || (y >= (1) && (!(x >= (1)) || (x >= (1) && !(x <= (2147483647))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && !(counter == (3))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && !(a == (2LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(q == (2LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && !(r >= (-2147483644LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (x >= (1) && x <= (2147483647) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL)))) && counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && !(counter == (0)) && (!(counter == (3)) || (counter == (3) && !(a == (2LL))) || (counter == (3) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(q == (2LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && !(r >= (-2147483644LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && !(x >= (1))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && x >= (1) && !(x <= (2147483647))) || (counter == (3) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && x >= (1) && x <= (2147483647) && !(y <= (1073741823)))) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && !(x >= (1))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && x >= (1) && !(x <= (2147483647)))) && counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r == ((long long int)x) && y <= (2147483647)) || (y >= (1) && (!(counter == (2)) || (counter == (2) && !(a == (1LL))) || (counter == (2) && a == (1LL) && !(b == ((long long int)y))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && !(q == (1LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && !(r >= (-2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && !(r <= (2147483646LL))) || (counter == (2) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && !(y <= (2147483647)))) && (!(counter == (0)) || (counter == (0) && !(a == (0LL))) || (counter == (0) && a == (0LL) && !(b == (0LL))) || (counter == (0) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (0) && a == (0LL) && b == (0LL) && q == (0LL) && !(r == ((long long int)x))) || (counter == (0) && a == (0LL) && b == (0LL) && q == (0LL) && r == ((long long int)x) && !(y <= (2147483647)))) && !(counter == (3)) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(b == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && !(r == ((long long int)x))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && r == ((long long int)x) && !(y <= (2147483647)))) && counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && x >= (1) && x <= (2147483647) && y <= (1073741823)) || (y >= (1) && !(counter == (2)) && (!(counter == (0)) || (counter == (0) && !(a == (0LL))) || (counter == (0) && a == (0LL) && !(b == (0LL))) || (counter == (0) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (0) && a == (0LL) && b == (0LL) && q == (0LL) && !(r == ((long long int)x)))) && (!(a == (2LL)) || (a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && !(q == (2LL))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && !(r >= (-2147483644LL))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && (!(counter == (1)) || (counter == (1) && !(a == (0LL))) || (counter == (1) && a == (0LL) && !(b == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && !(q == (0LL))) || (counter == (1) && a == (0LL) && b == (0LL) && q == (0LL) && !(r == ((long long int)x)))) && (!(counter == (4)) || (counter == (4) && !(a == (2LL))) || (counter == (4) && a == (2LL) && !(b == ((2LL) * ((long long int)y)))) || (counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && !(q == (2LL))) || (counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && !(r >= (-2147483644LL))) || (counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && !(r <= (2147483645LL))) || (counter == (4) && a == (2LL) && b == ((2LL) * ((long long int)y)) && q == (2LL) && r >= (-2147483644LL) && r <= (2147483645LL) && !(y <= (1073741823)))) && counter == (3) && a == (1LL) && b == ((long long int)y) && q == (1LL) && r >= (-2147483646LL) && r <= (2147483646LL) && x >= (1) && x <= (2147483647) && y <= (2147483647)) (../plain/cohendiv-ll_unwindbound2.c:37:5)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 2
  refuted: 2
  error: 4
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 8
SV-COMP result: false

vars = 157    evals = 515    narrow_reuses = 9

Timings:
                                  cputime   walltime   allocated   count
Default                            6.713s     6.760s    764.51MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.15MB      4×
  Cabs2cil                           0.005s     0.005s      4.79MB      4×
  mergeCIL                           0.004s     0.004s      3.35MB      1×
  analysis                           6.670s     6.716s    747.22MB      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.010s     0.011s      6.59MB      8×
    Cabs2cil                           0.017s     0.017s      6.94MB      8×
    global_inits                       0.001s     0.001s      0.18MB      1×
    solving                            2.442s     2.450s    623.63MB      1×
      S.Dom.equal                        0.001s     0.002s      0.18MB    524×
      base unassume                      0.403s     0.405s    385.56MB     44×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.036s     0.036s     22.25MB      1×
        postsolver_iter                    0.036s     0.036s     22.16MB      1×
    warn_global                        0.001s     0.001s      0.14MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
