/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/diamond_2-2.yml.witness.yml --witness.yaml.validate pesco/diamond_2-2.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/diamond_2-2.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 == (4294967291U) || (!(x == (4294967291U)) && x == (4294967292U)) || (!(x == (4294967291U)) && !(x == (4294967292U)) && x == (4294967295U)) (../plain/diamond_2-2.c:49:3)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((x == 15U || (! (x == 15U) && x == 24U)) || ((! (x == 15U) && ! (x == 24U)) && x == 25U)) || (((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && x == 19U)) || ((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && x == 9U)) || (((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && x == 14U)) || ((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && x == 8U)) || (((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && x == 1U)) || ((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && x == 16U)) || (((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && x == 4294967293U)) || ((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && x == 3U)) || (((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && x == 30U)) || ((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && x == 20U)) || (((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && x == 21U)) || ((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && x == 13U)) || (((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && x == 4294967295U)) || ((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && x == 31U)) || (((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && x == 4294967290U)) || ((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && x == 5U)) || (((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && x == 22U)) || ((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && x == 6U)) || (((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && x == 4294967292U)) || ((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && x == 4294967294U)) || (((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && x == 28U)) || ((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && x == 11U)) || (((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && x == 27U)) || ((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && x == 18U)) || (((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && x == 29U)) || ((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && x == 7U)) || (((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && x == 17U)) || ((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && x == 23U)) || (((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && x == 4294967291U)) || ((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && x == 2U)) || (((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && x == 0U)) || ((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && x == 10U)) || (((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && x == 26U)) || ((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && x == 4294967289U)) || (((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && x == 4U)) || ((((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && ! (x == 4U)) && x == 12U) (../plain/diamond_2-2.c:15:16-15:44)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:18:9-18:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:21:9-21:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:22:10-22:16)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:24:9-24:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:25:10-25:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:24:21-24:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:27:9-27:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:28:10-28:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:27:21-27:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:30:9-30:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:31:10-31:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:30:21-30:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:33:9-33:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:34:10-34:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:33:21-33:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:36:9-36:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:37:10-37:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:36:21-36:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:39:9-39:19)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:40:10-40:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:39:21-39:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:42:9-42:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:43:10-43:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:42:21-42:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:45:9-45:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/diamond_2-2.c:46:10-46:16)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((x == 15U || (! (x == 15U) && x == 24U)) || ((! (x == 15U) && ! (x == 24U)) && x == 25U)) || (((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && x == 19U)) || ((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && x == 9U)) || (((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && x == 14U)) || ((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && x == 8U)) || (((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && x == 1U)) || ((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && x == 16U)) || (((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && x == 4294967293U)) || ((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && x == 3U)) || (((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && x == 30U)) || ((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && x == 20U)) || (((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && x == 21U)) || ((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && x == 13U)) || (((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && x == 4294967295U)) || ((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && x == 31U)) || (((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && x == 4294967290U)) || ((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && x == 5U)) || (((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && x == 22U)) || ((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && x == 6U)) || (((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && x == 4294967292U)) || ((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && x == 4294967294U)) || (((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && x == 28U)) || ((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && x == 11U)) || (((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && x == 27U)) || ((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && x == 18U)) || (((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && x == 29U)) || ((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && x == 7U)) || (((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && x == 17U)) || ((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && x == 23U)) || (((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && x == 4294967291U)) || ((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && x == 2U)) || (((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && x == 0U)) || ((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && x == 10U)) || (((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && x == 26U)) || ((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && x == 4294967289U)) || (((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && x == 4U)) || ((((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && ! (x == 4U)) && x == 12U) (../plain/diamond_2-2.c:46:10-46:16)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/diamond_2-2.c:45:21-45:27)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((x == 15U || (! (x == 15U) && x == 24U)) || ((! (x == 15U) && ! (x == 24U)) && x == 25U)) || (((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && x == 19U)) || ((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && x == 9U)) || (((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && x == 14U)) || ((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && x == 8U)) || (((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && x == 1U)) || ((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && x == 16U)) || (((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && x == 4294967293U)) || ((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && x == 3U)) || (((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && x == 30U)) || ((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && x == 20U)) || (((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && x == 21U)) || ((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && x == 13U)) || (((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && x == 4294967295U)) || ((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && x == 31U)) || (((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && x == 4294967290U)) || ((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && x == 5U)) || (((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && x == 22U)) || ((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && x == 6U)) || (((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && x == 4294967292U)) || ((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && x == 4294967294U)) || (((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && x == 28U)) || ((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && x == 11U)) || (((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && x == 27U)) || ((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && x == 18U)) || (((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && x == 29U)) || ((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && x == 7U)) || (((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && x == 17U)) || ((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && x == 23U)) || (((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && x == 4294967291U)) || ((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && x == 2U)) || (((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && x == 0U)) || ((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && x == 10U)) || (((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && x == 26U)) || ((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && x == 4294967289U)) || (((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && x == 4U)) || ((((((((((((((((((((((((((((((((((((((! (x == 15U) && ! (x == 24U)) && ! (x == 25U)) && ! (x == 19U)) && ! (x == 9U)) && ! (x == 14U)) && ! (x == 8U)) && ! (x == 1U)) && ! (x == 16U)) && ! (x == 4294967293U)) && ! (x == 3U)) && ! (x == 30U)) && ! (x == 20U)) && ! (x == 21U)) && ! (x == 13U)) && ! (x == 4294967295U)) && ! (x == 31U)) && ! (x == 4294967290U)) && ! (x == 5U)) && ! (x == 22U)) && ! (x == 6U)) && ! (x == 4294967292U)) && ! (x == 4294967294U)) && ! (x == 28U)) && ! (x == 11U)) && ! (x == 27U)) && ! (x == 18U)) && ! (x == 29U)) && ! (x == 7U)) && ! (x == 17U)) && ! (x == 23U)) && ! (x == 4294967291U)) && ! (x == 2U)) && ! (x == 0U)) && ! (x == 10U)) && ! (x == 26U)) && ! (x == 4294967289U)) && ! (x == 4U)) && x == 12U) (../plain/diamond_2-2.c:45:21-45:27)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 32
  dead: 0
  total lines: 32
[Warning][Witness] invariant unconfirmed: x == (15U) || (!(x == (15U)) && x == (24U)) || (!(x == (15U)) && !(x == (24U)) && x == (25U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && x == (19U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && x == (9U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && x == (14U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && x == (8U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && x == (1U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && x == (16U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && x == (4294967293U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && x == (3U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && x == (30U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && x == (20U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && x == (21U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && x == (13U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && x == (4294967295U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && x == (31U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && x == (4294967290U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && x == (5U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && x == (22U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && x == (6U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && x == (4294967292U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && x == (4294967294U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && x == (28U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && x == (11U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && x == (27U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && x == (18U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && x == (29U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && x == (7U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && x == (17U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && x == (23U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && x == (4294967291U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && x == (2U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && x == (0U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && !(x == (0U)) && x == (10U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && !(x == (0U)) && !(x == (10U)) && x == (26U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && !(x == (0U)) && !(x == (10U)) && !(x == (26U)) && x == (4294967289U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && !(x == (0U)) && !(x == (10U)) && !(x == (26U)) && !(x == (4294967289U)) && x == (4U)) || (!(x == (15U)) && !(x == (24U)) && !(x == (25U)) && !(x == (19U)) && !(x == (9U)) && !(x == (14U)) && !(x == (8U)) && !(x == (1U)) && !(x == (16U)) && !(x == (4294967293U)) && !(x == (3U)) && !(x == (30U)) && !(x == (20U)) && !(x == (21U)) && !(x == (13U)) && !(x == (4294967295U)) && !(x == (31U)) && !(x == (4294967290U)) && !(x == (5U)) && !(x == (22U)) && !(x == (6U)) && !(x == (4294967292U)) && !(x == (4294967294U)) && !(x == (28U)) && !(x == (11U)) && !(x == (27U)) && !(x == (18U)) && !(x == (29U)) && !(x == (7U)) && !(x == (17U)) && !(x == (23U)) && !(x == (4294967291U)) && !(x == (2U)) && !(x == (0U)) && !(x == (10U)) && !(x == (26U)) && !(x == (4294967289U)) && !(x == (4U)) && x == (12U)) (../plain/diamond_2-2.c:17:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 2
SV-COMP result: unknown

vars = 65    evals = 109    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            2.526s     2.537s    417.86MB      1×
  preprocess                         0.026s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.14MB      4×
  Cabs2cil                           0.006s     0.006s      4.77MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           2.482s     2.494s    400.59MB      1×
    createCFG                          0.001s     0.001s      0.64MB      1×
      handle                             0.001s     0.001s      0.11MB     33×
      iter_connect                       0.001s     0.001s      0.41MB     33×
        computeSCCs                        0.001s     0.001s      0.24MB     34×
    FrontC                             0.011s     0.011s      6.03MB      2×
    Cabs2cil                           0.004s     0.004s      4.50MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.806s     0.806s    298.09MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB    110×
      base unassume                      0.180s     0.180s    211.46MB      7×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.025s     0.025s     21.33MB      1×
        postsolver_iter                    0.025s     0.025s     21.28MB      1×
    warn_global                        0.001s     0.001s      0.21MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
