/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 /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/aiob_4.c.v+lhb-reducer.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/aiob_4.c.v+lhb-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/aiob_4.c.v+lhb-reducer.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: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:417:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:417:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:417:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:417:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:418:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:418:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:418:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:418:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:420:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:420:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:420:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:420:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:423:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:423:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:423:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:423:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:425:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:425:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:425:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:425:6)
[Warning][Witness] couldn't locate invariant: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:425:6)
[Warning][Witness] couldn't locate invariant: 41LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:427:2)
[Warning][Witness] couldn't locate invariant: 41LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: 41LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:432:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:433:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:433:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:433:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:433:6)
[Warning][Witness] couldn't locate invariant: Id_MCDC_93 <= 41U (../plain/aiob_4.c.v+lhb-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:440:7)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:440:7)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:440:7)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:440:7)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:442:9)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:442:9)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:442:9)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:442:9)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:443:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:443:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:443:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:443:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:445:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:445:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:445:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:445:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:446:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:446:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:446:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:446:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:447:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:447:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:447:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:447:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:452:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:452:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:452:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:452:2)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:459:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:459:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:459:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:459:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:459:2)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:462:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:462:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:462:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:462:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:462:2)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:464:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:464:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:464:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:464:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:464:2)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:465:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:465:6)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:465:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:465:6)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:465:6)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:467:3)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:467:3)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:467:3)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:467:3)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:467:3)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_93 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: -42LL + (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:468:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:484:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:484:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:484:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:484:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:501:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:501:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:501:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:501:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:518:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:518:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:518:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:518:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:535:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:535:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:535:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:535:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:552:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:552:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:552:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:552:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:569:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:569:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:569:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:569:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:586:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:586:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:586:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:586:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:603:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:603:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:603:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:603:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:620:2)
[Warning][Witness] couldn't locate invariant: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:620:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:620:2)
[Warning][Witness] couldn't locate invariant: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:620:2)

runtime: 00:00:15.449
vars: 13, evals: 6

|rho|=13
|called|=5
|stable|=13
|infl|=3
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=6
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=348.02MB, max=22.25MB, minor=340.38MB, major=44.52MB, promoted=36.88MB
    minor collections=172  major collections=10 compactions=0


runtime: 00:00:21.176
vars: 14, evals: 6

|rho|=14
|called|=2
|stable|=14
|infl|=7
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=6
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=348.64MB, max=22.25MB, minor=340.99MB, major=44.54MB, promoted=36.89MB
    minor collections=177  major collections=11 compactions=0


runtime: 00:00:30.761
vars: 193, evals: 184

|rho|=193
|called|=155
|stable|=193
|infl|=33
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=370.62MB, max=22.25MB, minor=362.97MB, major=45.03MB, promoted=37.38MB
    minor collections=203  major collections=15 compactions=0


runtime: 00:00:40.644
vars: 193, evals: 184

|rho|=193
|called|=115
|stable|=193
|infl|=73
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=491.50MB, max=22.25MB, minor=483.85MB, major=46.57MB, promoted=38.91MB
    minor collections=274  major collections=27 compactions=0


runtime: 00:00:50.625
vars: 193, evals: 184

|rho|=193
|called|=79
|stable|=193
|infl|=109
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=685.75MB, max=22.25MB, minor=678.09MB, major=48.80MB, promoted=41.14MB
    minor collections=388  major collections=39 compactions=0


runtime: 00:01:00.682
vars: 193, evals: 184

|rho|=193
|called|=43
|stable|=193
|infl|=145
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=940.22MB, max=22.25MB, minor=932.55MB, major=51.68MB, promoted=44.01MB
    minor collections=527  major collections=49 compactions=0


runtime: 00:01:10.705
vars: 193, evals: 184

|rho|=193
|called|=9
|stable|=193
|infl|=179
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1241.73MB, max=22.25MB, minor=1234.06MB, major=54.94MB, promoted=47.27MB
    minor collections=688  major collections=59 compactions=0


runtime: 00:01:20.655
vars: 227, evals: 208

|rho|=227
|called|=5
|stable|=227
|infl|=217
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=208
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1365.73MB, max=22.25MB, minor=1358.05MB, major=56.38MB, promoted=48.71MB
    minor collections=766  major collections=65 compactions=0


runtime: 00:01:36.234
vars: 350, evals: 581

|rho|=350
|called|=287
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2080.26MB, max=29.42MB, minor=2072.57MB, major=81.79MB, promoted=74.10MB
    minor collections=1115  major collections=70 compactions=0


runtime: 00:01:40.854
vars: 350, evals: 581

|rho|=350
|called|=286
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2080.53MB, max=29.42MB, minor=2072.84MB, major=81.80MB, promoted=74.11MB
    minor collections=1118  major collections=70 compactions=0


runtime: 00:01:50.740
vars: 350, evals: 581

|rho|=350
|called|=254
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2112.53MB, max=29.42MB, minor=2104.84MB, major=82.05MB, promoted=74.36MB
    minor collections=1146  major collections=75 compactions=0


runtime: 00:02:00.861
vars: 350, evals: 581

|rho|=350
|called|=217
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2246.27MB, max=29.42MB, minor=2238.58MB, major=83.52MB, promoted=75.83MB
    minor collections=1223  major collections=85 compactions=0


runtime: 00:02:10.783
vars: 350, evals: 581

|rho|=350
|called|=182
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2446.36MB, max=29.42MB, minor=2438.67MB, major=85.63MB, promoted=77.94MB
    minor collections=1335  major collections=96 compactions=0


runtime: 00:02:20.793
vars: 350, evals: 581

|rho|=350
|called|=148
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2688.47MB, max=29.42MB, minor=2680.78MB, major=88.21MB, promoted=80.52MB
    minor collections=1471  major collections=106 compactions=0


runtime: 00:02:30.923
vars: 350, evals: 581

|rho|=350
|called|=114
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2996.89MB, max=29.42MB, minor=2989.20MB, major=91.37MB, promoted=83.68MB
    minor collections=1636  major collections=116 compactions=0


runtime: 00:02:40.778
vars: 350, evals: 581

|rho|=350
|called|=89
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=3121.42MB, max=29.42MB, minor=3113.73MB, major=92.65MB, promoted=84.96MB
    minor collections=1711  major collections=121 compactions=0


runtime: 00:02:50.795
vars: 354, evals: 666

|rho|=354
|called|=12
|stable|=343
|infl|=348
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=7079.68MB, max=59.18MB, minor=7071.89MB, major=327.39MB, promoted=319.60MB
    minor collections=3642  major collections=140 compactions=0


runtime: 00:03:00.813
vars: 395, evals: 733

|rho|=395
|called|=1
|stable|=395
|infl|=391
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8571.76MB, max=59.18MB, minor=8563.95MB, major=374.18MB, promoted=366.36MB
    minor collections=4384  major collections=153 compactions=1


runtime: 00:03:18.778
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=1
|side_infl|=1
|var_messages|=0
|rho_write|=1
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8628.41MB, max=59.18MB, minor=8620.59MB, major=374.57MB, promoted=366.75MB
    minor collections=4421  major collections=155 compactions=1


runtime: 00:03:22.799
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=1
|side_infl|=1
|var_messages|=0
|rho_write|=1
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8628.69MB, max=59.18MB, minor=8620.88MB, major=374.58MB, promoted=366.76MB
    minor collections=4425  major collections=156 compactions=1

[Info][Imprecise] Invalidating expressions: AddrOf(Var(main__Id_MCDC_112, NoOffset)) (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)
[Info][Unsound] Unknown address in {&main__Id_MCDC_112} has escaped. (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)

runtime: 00:03:31.067
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8632.29MB, max=59.18MB, minor=8624.47MB, major=374.85MB, promoted=367.03MB
    minor collections=4445  major collections=158 compactions=1


runtime: 00:03:41.175
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8645.54MB, max=59.18MB, minor=8637.72MB, major=374.96MB, promoted=367.15MB
    minor collections=4472  major collections=162 compactions=1


runtime: 00:03:51.149
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8673.64MB, max=59.18MB, minor=8665.82MB, major=375.16MB, promoted=367.34MB
    minor collections=4499  major collections=166 compactions=1


runtime: 00:04:01.199
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8723.54MB, max=59.18MB, minor=8715.73MB, major=375.67MB, promoted=367.86MB
    minor collections=4539  major collections=172 compactions=1


runtime: 00:04:11.370
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8785.06MB, max=59.18MB, minor=8777.25MB, major=376.30MB, promoted=368.48MB
    minor collections=4589  major collections=179 compactions=1


runtime: 00:04:21.398
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8860.32MB, max=59.18MB, minor=8852.51MB, major=377.04MB, promoted=369.22MB
    minor collections=4645  major collections=188 compactions=1


runtime: 00:04:31.487
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=8945.40MB, max=59.18MB, minor=8937.58MB, major=377.89MB, promoted=370.07MB
    minor collections=4707  major collections=199 compactions=1


runtime: 00:04:41.514
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9032.02MB, max=59.18MB, minor=9024.21MB, major=378.76MB, promoted=370.94MB
    minor collections=4767  major collections=209 compactions=1


runtime: 00:04:51.644
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9132.22MB, max=59.18MB, minor=9124.40MB, major=379.77MB, promoted=371.95MB
    minor collections=4835  major collections=221 compactions=1


runtime: 00:05:01.671
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9241.38MB, max=59.18MB, minor=9233.56MB, major=380.87MB, promoted=373.05MB
    minor collections=4907  major collections=235 compactions=1


runtime: 00:05:11.869
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9362.97MB, max=59.18MB, minor=9355.15MB, major=382.08MB, promoted=374.26MB
    minor collections=4991  major collections=250 compactions=1


runtime: 00:05:21.936
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9497.21MB, max=59.18MB, minor=9489.39MB, major=383.37MB, promoted=375.55MB
    minor collections=5076  major collections=264 compactions=1


runtime: 00:05:32.157
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=5
|side_infl|=6
|var_messages|=3
|rho_write|=4
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9604.76MB, max=59.18MB, minor=9596.94MB, major=384.39MB, promoted=376.57MB
    minor collections=5150  major collections=276 compactions=1


runtime: 00:05:42.061
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=14
|side_infl|=19
|var_messages|=3
|rho_write|=15
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=9752.45MB, max=59.18MB, minor=9744.63MB, major=385.79MB, promoted=377.97MB
    minor collections=5241  major collections=291 compactions=1

[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((long long )main__Id_MCDC_114 >= 0LL && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && Id_MCDC_93 <= 41U) && -42LL + (long long )Id_MCDC_93 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_116 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_116 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_116 >= 0LL) && (long long )main__Id_MCDC_115 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_116 >= 0LL) && 65535LL - (long long )main__Id_MCDC_115 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && -42LL + (long long )Id_MCDC_93 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:414:2-414:47)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/aiob_4.c.v+lhb-reducer.c:443:2-443:53)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((long long )main__Id_MCDC_114 >= 0LL && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && Id_MCDC_93 <= 41U) && -42LL + (long long )Id_MCDC_93 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_116 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_116 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_116 >= 0LL) && (long long )main__Id_MCDC_115 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_116 >= 0LL) && 65535LL - (long long )main__Id_MCDC_115 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && -42LL + (long long )Id_MCDC_93 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL) && (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && (long long )main__Id_MCDC_114 >= 0LL) && (long long )main__Id_MCDC_113 >= 0LL) && 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL) && 65535LL - (long long )main__Id_MCDC_114 >= 0LL) && 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:447:2-447:47)
[Warning][Deadcode] Function 'main' has dead code:
  on line 194 (../plain/aiob_4.c.v+lhb-reducer.c:194-194)
  on line 220 (../plain/aiob_4.c.v+lhb-reducer.c:220-220)
  on line 246 (../plain/aiob_4.c.v+lhb-reducer.c:246-246)
  on line 272 (../plain/aiob_4.c.v+lhb-reducer.c:272-272)
  on line 298 (../plain/aiob_4.c.v+lhb-reducer.c:298-298)
  on line 324 (../plain/aiob_4.c.v+lhb-reducer.c:324-324)
  on line 350 (../plain/aiob_4.c.v+lhb-reducer.c:350-350)
  on line 376 (../plain/aiob_4.c.v+lhb-reducer.c:376-376)
  on line 402 (../plain/aiob_4.c.v+lhb-reducer.c:402-402)
  on line 435 (../plain/aiob_4.c.v+lhb-reducer.c:435-435)
  on line 472 (../plain/aiob_4.c.v+lhb-reducer.c:472-472)
  on line 479 (../plain/aiob_4.c.v+lhb-reducer.c:479-479)
  on line 491 (../plain/aiob_4.c.v+lhb-reducer.c:491-491)
  on line 496 (../plain/aiob_4.c.v+lhb-reducer.c:496-496)
  on line 508 (../plain/aiob_4.c.v+lhb-reducer.c:508-508)
  on line 513 (../plain/aiob_4.c.v+lhb-reducer.c:513-513)
  on line 525 (../plain/aiob_4.c.v+lhb-reducer.c:525-525)
  on line 530 (../plain/aiob_4.c.v+lhb-reducer.c:530-530)
  on line 542 (../plain/aiob_4.c.v+lhb-reducer.c:542-542)
  on line 547 (../plain/aiob_4.c.v+lhb-reducer.c:547-547)
  on line 559 (../plain/aiob_4.c.v+lhb-reducer.c:559-559)
  on line 564 (../plain/aiob_4.c.v+lhb-reducer.c:564-564)
  on line 576 (../plain/aiob_4.c.v+lhb-reducer.c:576-576)
  on line 581 (../plain/aiob_4.c.v+lhb-reducer.c:581-581)
  on line 593 (../plain/aiob_4.c.v+lhb-reducer.c:593-593)
  on line 598 (../plain/aiob_4.c.v+lhb-reducer.c:598-598)
  on line 610 (../plain/aiob_4.c.v+lhb-reducer.c:610-610)
  on line 615 (../plain/aiob_4.c.v+lhb-reducer.c:615-615)
  on line 627 (../plain/aiob_4.c.v+lhb-reducer.c:627-627)
  on line 632 (../plain/aiob_4.c.v+lhb-reducer.c:632-632)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 147
  dead: 30
  total lines: 177
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:364:6-364:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:366:6-366:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___6 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:374:6-374:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:390:6-390:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:392:6-392:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___7 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:400:6-400:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:182:6-182:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:184:6-184:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:192:6-192:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:423:6-423:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:208:6-208:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:210:6-210:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___8 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:433:6-433:40)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___0 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:218:6-218:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:234:6-234:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:236:6-236:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___1 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:244:6-244:40)
[Warning][Deadcode][CWE-571] condition '__VERIFIER_assert__Id_MCDC_92___9 == 0' is always true (../plain/aiob_4.c.v+lhb-reducer.c:465:6-465:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:260:6-260:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:262:6-262:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___2 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:270:6-270:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:286:6-286:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:288:6-288:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___3 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:296:6-296:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:312:6-312:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:314:6-314:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___4 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:322:6-322:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:338:6-338:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:340:6-340:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___5 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:348:6-348:40)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:177:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:179:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:179:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:179:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:179:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:182:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:182:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:182:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:182:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:184:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:184:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:184:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:184:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:186:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:186:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:186:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:186:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:189:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:189:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:189:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:189:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:191:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:191:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:191:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:191:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:192:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:192:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:192:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:192:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:198:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:198:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:198:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:198:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:199:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:199:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:199:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:199:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:201:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:201:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:201:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:201:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:205:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:205:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:205:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:205:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:208:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:208:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:208:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:208:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:210:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:210:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:210:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:210:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:212:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:212:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:212:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:212:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:215:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:215:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:215:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:215:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:217:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:217:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:217:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:217:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:218:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:218:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:218:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:218:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:224:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:224:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:224:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:224:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:225:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:225:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:225:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:225:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:227:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:227:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:227:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:227:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:228:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:228:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:228:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:228:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:234:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:234:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:234:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:234:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:236:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:236:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:236:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:236:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:238:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:238:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:238:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:238:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:241:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:241:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:241:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:241:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:243:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:243:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:243:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:243:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:244:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:244:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:244:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:244:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:250:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:250:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:250:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:250:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:251:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:251:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:251:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:251:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:253:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:253:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:253:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:253:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:254:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:254:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:254:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:254:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:257:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:257:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:257:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:257:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:260:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:260:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:260:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:260:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:262:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:262:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:262:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:262:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:267:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:267:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:267:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:267:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:269:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:269:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:269:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:269:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:270:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:270:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:270:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:270:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:276:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:276:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:276:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:276:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:277:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:277:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:277:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:277:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:279:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:279:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:279:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:279:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:280:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:280:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:280:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:280:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:283:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:283:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:283:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:283:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:286:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:286:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:286:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:286:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:288:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:288:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:288:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:288:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:290:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:290:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:290:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:290:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:293:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:293:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:293:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:293:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:295:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:295:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:295:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:295:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:296:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:296:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:296:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:296:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:302:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:302:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:302:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:302:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:303:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:303:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:303:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:303:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:305:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:305:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:305:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:305:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:309:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:309:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:309:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:309:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:312:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:312:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:312:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:312:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:314:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:314:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:314:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:314:6)
[Error][Witness] invariant refuted: -42LL + (long long )Id_MCDC_93 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:4:22)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:316:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:316:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:316:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:316:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_115 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_116 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_115 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_116 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:156:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:319:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:319:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:319:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:319:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_116 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_116 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:157:17)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:321:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:321:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:321:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:321:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:322:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:322:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:322:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:322:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:166:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:328:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:328:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:328:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:328:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:329:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:329:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:329:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:329:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:172:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:174:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:331:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:331:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:331:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:331:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:175:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:332:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:332:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:332:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:332:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:335:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:335:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:335:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:335:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:338:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:338:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:338:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:338:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:340:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:340:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:340:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:340:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:342:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:342:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:342:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:342:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:345:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:345:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:345:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:345:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:347:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:347:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:347:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:347:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:348:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:348:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:348:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:348:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:354:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:354:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:354:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:354:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:355:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:355:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:355:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:355:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:357:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:357:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:357:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:357:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:358:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:358:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:358:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:358:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:361:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:361:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:361:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:361:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:364:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:364:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:364:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:364:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:366:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:366:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:366:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:366:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:368:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:368:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:368:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:368:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:371:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:371:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:371:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:371:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:373:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:373:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:373:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:373:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:374:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:374:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:374:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:374:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:380:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:380:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:380:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:380:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:381:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:381:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:381:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:381:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:383:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:383:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:383:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:383:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:384:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:384:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:384:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:384:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:387:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:387:2)

runtime: 00:05:52.130
vars: 395, evals: 733

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=50
|side_infl|=104
|var_messages|=6
|rho_write|=86
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=11056.68MB, max=59.18MB, minor=11044.37MB, major=427.20MB, promoted=414.88MB
    minor collections=5881  major collections=302 compactions=1

[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:387:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:387:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:390:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:390:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:390:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:390:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:392:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:392:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:392:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:392:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:394:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:394:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:394:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:394:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:397:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:397:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:397:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:397:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:399:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:399:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:399:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:399:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:400:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:400:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:400:6)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:400:6)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: 4294967295LL - (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: (long long )Id_MCDC_89__Id_MCDC_96 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:176:15)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:406:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:406:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:406:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:406:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:407:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:407:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:407:7)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:407:7)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:409:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:409:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:409:9)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:409:9)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:410:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:410:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:410:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:410:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:412:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:412:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:412:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:412:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:413:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:413:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:413:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:413:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:414:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:414:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:414:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:414:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:416:2)
[Success][Witness] invariant confirmed: 65535LL - (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:416:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_113 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:416:2)
[Success][Witness] invariant confirmed: (long long )main__Id_MCDC_114 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:416:2)
[Error][Witness] invariant refuted: -42LL + (long long )Id_MCDC_93 >= 0LL (../plain/aiob_4.c.v+lhb-reducer.c:4:1)
[Success][Witness] invariant confirmed: Id_MCDC_93 <= 41U (../plain/aiob_4.c.v+lhb-reducer.c:416:2)
[Info][Witness] witness validation summary:
  confirmed: 483
  unconfirmed: 0
  refuted: 2
  error: 143
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 628
SV-COMP result: false

vars = 395    evals = 733    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                          352.350s   352.368s  11076.91MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.55MB      4×
  Cabs2cil                           0.006s     0.006s      7.28MB      4×
  mergeCIL                           0.003s     0.003s      3.66MB      1×
  analysis                         352.305s   352.324s  11054.88MB      1×
    createCFG                          0.005s     0.005s      1.55MB      1×
      handle                             0.003s     0.003s      0.36MB     32×
      iter_connect                       0.001s     0.001s      1.02MB     32×
        computeSCCs                        0.001s     0.001s      0.74MB     33×
    FrontC                             0.025s     0.027s      7.39MB    970×
    Cabs2cil                           0.237s     0.238s     93.35MB    970×
    global_inits                       0.001s     0.001s      0.60MB      1×
    solving                          350.506s   350.523s  10351.15MB      1×
      S.Dom.equal                        0.003s     0.006s      0.25MB    734×
      base unassume                      2.243s     2.243s   1250.85MB     14×
      cheap_full_reach                   0.001s     0.001s      0.19MB      1×
      postsolver                       169.414s   169.422s   2070.75MB      1×
        postsolver_iter                  169.413s   169.422s   2070.44MB      1×
    warn_global                        0.001s     0.001s      1.27MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
