/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-self2/ourtool.2023-02-15_09-12-33.files/ourtool/ps3-ll_valuebound50.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/ps3-ll_valuebound50.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/ps3-ll_valuebound50.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: 0LL <= y (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:28:9)
[Warning][Witness] couldn't locate invariant: 0LL <= c (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: c <= 32767LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:30:13)
[Warning][Witness] couldn't locate invariant: 0LL <= c (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: c <= 32766LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (-1LL - c) + (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:33:9)
[Warning][Witness] couldn't locate invariant: 0LL <= y (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 1LL <= c (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: c <= 32767LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: -1LL + c >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (0LL - c) + (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (10LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (15LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (21LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (28LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (36LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (45LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (55LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (66LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (78LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (91LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (105LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (120LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (136LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (153LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (171LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (190LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (210LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (231LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (253LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (276LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (300LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (325LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (351LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (378LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (406LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (435LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (465LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (496LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (528LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (561LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (595LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (630LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (666LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (703LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (741LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (780LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (820LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (861LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (903LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (946LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (990LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1035LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1081LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1128LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1176LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1225LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1275LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1326LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1378LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1431LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1485LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1540LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1596LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1653LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1711LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1770LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1830LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1891LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1953LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2016LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2080LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2145LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2211LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2278LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2346LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2415LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2485LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2556LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2628LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2701LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2775LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2850LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (2926LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3003LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3081LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3160LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3240LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3321LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3403LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3486LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3570LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3655LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3741LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3828LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (3916LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4005LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4095LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4186LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4278LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4371LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4465LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4560LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4656LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4753LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4851LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (4950LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5050LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5151LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5253LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5356LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5460LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5565LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5671LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5778LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5886LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (5995LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6105LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6216LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6328LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6441LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6555LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6670LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6786LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (6903LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7021LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7140LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7260LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7381LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7503LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (7626LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: -1LL + c >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (0LL - c) + (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (10LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (15LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (21LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (28LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (36LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (45LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (55LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (66LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (78LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (91LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (105LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (120LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (136LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (153LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (171LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (190LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (210LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (231LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (253LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (276LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (300LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (325LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (351LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (378LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (406LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (435LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (465LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (496LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (528LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (561LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (595LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (630LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (666LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (703LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (741LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (780LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (820LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (861LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (903LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (946LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (990LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1035LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1081LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1128LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1176LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1225LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1275LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1326LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1378LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1431LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1485LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1540LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1596LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1653LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1711LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1770LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1830LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1891LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1953LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2016LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2080LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2145LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2211LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2278LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2346LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2415LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2485LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2556LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2628LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2701LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2775LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2850LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (2926LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3003LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3081LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3160LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3240LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3321LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3403LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3486LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3570LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3655LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3741LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3828LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (3916LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4005LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4095LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4186LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4278LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4371LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4465LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4560LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4656LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4753LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4851LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (4950LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5050LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5151LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5253LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5356LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5460LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5565LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5671LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5778LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5886LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (5995LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6105LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6216LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6328LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6441LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6555LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6670LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6786LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (6903LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7021LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7140LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7260LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7381LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7503LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (7626LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 0LL <= y (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: c - (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:37:5)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Warning][Witness] couldn't locate invariant: c - (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:38:5)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((7503LL - 123LL * c) + x >= 0LL && (7381LL - 122LL * c) + x >= 0LL) && (7260LL - 121LL * c) + x >= 0LL) && (7140LL - 120LL * c) + x >= 0LL) && (7021LL - 119LL * c) + x >= 0LL) && (6903LL - 118LL * c) + x >= 0LL) && (6786LL - 117LL * c) + x >= 0LL) && (6670LL - 116LL * c) + x >= 0LL) && (6555LL - 115LL * c) + x >= 0LL) && (6441LL - 114LL * c) + x >= 0LL) && (6328LL - 113LL * c) + x >= 0LL) && (6216LL - 112LL * c) + x >= 0LL) && (6105LL - 111LL * c) + x >= 0LL) && (5995LL - 110LL * c) + x >= 0LL) && (5886LL - 109LL * c) + x >= 0LL) && (5778LL - 108LL * c) + x >= 0LL) && (5671LL - 107LL * c) + x >= 0LL) && (5565LL - 106LL * c) + x >= 0LL) && (5460LL - 105LL * c) + x >= 0LL) && (5356LL - 104LL * c) + x >= 0LL) && (5253LL - 103LL * c) + x >= 0LL) && (5151LL - 102LL * c) + x >= 0LL) && (5050LL - 101LL * c) + x >= 0LL) && (4950LL - 100LL * c) + x >= 0LL) && (4851LL - 99LL * c) + x >= 0LL) && (4753LL - 98LL * c) + x >= 0LL) && (4656LL - 97LL * c) + x >= 0LL) && (4560LL - 96LL * c) + x >= 0LL) && (4465LL - 95LL * c) + x >= 0LL) && (4371LL - 94LL * c) + x >= 0LL) && (4278LL - 93LL * c) + x >= 0LL) && (4186LL - 92LL * c) + x >= 0LL) && (4095LL - 91LL * c) + x >= 0LL) && (4005LL - 90LL * c) + x >= 0LL) && (3916LL - 89LL * c) + x >= 0LL) && (3828LL - 88LL * c) + x >= 0LL) && (3741LL - 87LL * c) + x >= 0LL) && (3655LL - 86LL * c) + x >= 0LL) && (3570LL - 85LL * c) + x >= 0LL) && (3486LL - 84LL * c) + x >= 0LL) && (3403LL - 83LL * c) + x >= 0LL) && (3321LL - 82LL * c) + x >= 0LL) && (3240LL - 81LL * c) + x >= 0LL) && (3160LL - 80LL * c) + x >= 0LL) && (3081LL - 79LL * c) + x >= 0LL) && (3003LL - 78LL * c) + x >= 0LL) && (2926LL - 77LL * c) + x >= 0LL) && (2850LL - 76LL * c) + x >= 0LL) && (2775LL - 75LL * c) + x >= 0LL) && (2701LL - 74LL * c) + x >= 0LL) && (2628LL - 73LL * c) + x >= 0LL) && (2556LL - 72LL * c) + x >= 0LL) && (2485LL - 71LL * c) + x >= 0LL) && (2415LL - 70LL * c) + x >= 0LL) && (2346LL - 69LL * c) + x >= 0LL) && (2278LL - 68LL * c) + x >= 0LL) && (2211LL - 67LL * c) + x >= 0LL) && (2145LL - 66LL * c) + x >= 0LL) && (2080LL - 65LL * c) + x >= 0LL) && (2016LL - 64LL * c) + x >= 0LL) && (1953LL - 63LL * c) + x >= 0LL) && (1891LL - 62LL * c) + x >= 0LL) && (1830LL - 61LL * c) + x >= 0LL) && (1770LL - 60LL * c) + x >= 0LL) && (1711LL - 59LL * c) + x >= 0LL) && (1653LL - 58LL * c) + x >= 0LL) && (1596LL - 57LL * c) + x >= 0LL) && (1540LL - 56LL * c) + x >= 0LL) && (1485LL - 55LL * c) + x >= 0LL) && (1431LL - 54LL * c) + x >= 0LL) && (1378LL - 53LL * c) + x >= 0LL) && (1326LL - 52LL * c) + x >= 0LL) && (1275LL - 51LL * c) + x >= 0LL) && (1225LL - 50LL * c) + x >= 0LL) && (1176LL - 49LL * c) + x >= 0LL) && (1128LL - 48LL * c) + x >= 0LL) && (1081LL - 47LL * c) + x >= 0LL) && (1035LL - 46LL * c) + x >= 0LL) && (990LL - 45LL * c) + x >= 0LL) && (946LL - 44LL * c) + x >= 0LL) && (903LL - 43LL * c) + x >= 0LL) && (861LL - 42LL * c) + x >= 0LL) && (820LL - 41LL * c) + x >= 0LL) && (780LL - 40LL * c) + x >= 0LL) && (741LL - 39LL * c) + x >= 0LL) && (703LL - 38LL * c) + x >= 0LL) && (666LL - 37LL * c) + x >= 0LL) && (630LL - 36LL * c) + x >= 0LL) && (595LL - 35LL * c) + x >= 0LL) && (561LL - 34LL * c) + x >= 0LL) && (528LL - 33LL * c) + x >= 0LL) && (496LL - 32LL * c) + x >= 0LL) && (465LL - 31LL * c) + x >= 0LL) && (435LL - 30LL * c) + x >= 0LL) && (406LL - 29LL * c) + x >= 0LL) && (378LL - 28LL * c) + x >= 0LL) && (351LL - 27LL * c) + x >= 0LL) && (325LL - 26LL * c) + x >= 0LL) && (300LL - 25LL * c) + x >= 0LL) && (276LL - 24LL * c) + x >= 0LL) && (253LL - 23LL * c) + x >= 0LL) && (231LL - 22LL * c) + x >= 0LL) && (210LL - 21LL * c) + x >= 0LL) && (190LL - 20LL * c) + x >= 0LL) && (171LL - 19LL * c) + x >= 0LL) && (153LL - 18LL * c) + x >= 0LL) && (136LL - 17LL * c) + x >= 0LL) && (120LL - 16LL * c) + x >= 0LL) && (105LL - 15LL * c) + x >= 0LL) && (91LL - 14LL * c) + x >= 0LL) && (78LL - 13LL * c) + x >= 0LL) && (66LL - 12LL * c) + x >= 0LL) && (55LL - 11LL * c) + x >= 0LL) && (45LL - 10LL * c) + x >= 0LL) && (36LL - 9LL * c) + x >= 0LL) && (28LL - 8LL * c) + x >= 0LL) && (21LL - 7LL * c) + x >= 0LL) && (15LL - 6LL * c) + x >= 0LL) && (10LL - 5LL * c) + x >= 0LL) && (6LL - 4LL * c) + x >= 0LL) && (3LL - 3LL * c) + x >= 0LL) && (1LL - 2LL * c) + x >= 0LL) && (0LL - c) + x >= 0LL) && c >= 0LL) && c <= 32767LL) && 0LL <= c) && 0LL <= x) && 0LL <= y) && (long long )k >= 0LL) && 0 <= (int )k (../plain/ps3-ll_valuebound50.c:25:5-25:10)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps3-ll_valuebound50.c:28:9-28:58)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/ps3-ll_valuebound50.c:28:9-28:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps3-ll_valuebound50.c:34:9-34:18)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps3-ll_valuebound50.c:35:9-35:22)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((7503LL - 123LL * c) + x >= 0LL && (7381LL - 122LL * c) + x >= 0LL) && (7260LL - 121LL * c) + x >= 0LL) && (7140LL - 120LL * c) + x >= 0LL) && (7021LL - 119LL * c) + x >= 0LL) && (6903LL - 118LL * c) + x >= 0LL) && (6786LL - 117LL * c) + x >= 0LL) && (6670LL - 116LL * c) + x >= 0LL) && (6555LL - 115LL * c) + x >= 0LL) && (6441LL - 114LL * c) + x >= 0LL) && (6328LL - 113LL * c) + x >= 0LL) && (6216LL - 112LL * c) + x >= 0LL) && (6105LL - 111LL * c) + x >= 0LL) && (5995LL - 110LL * c) + x >= 0LL) && (5886LL - 109LL * c) + x >= 0LL) && (5778LL - 108LL * c) + x >= 0LL) && (5671LL - 107LL * c) + x >= 0LL) && (5565LL - 106LL * c) + x >= 0LL) && (5460LL - 105LL * c) + x >= 0LL) && (5356LL - 104LL * c) + x >= 0LL) && (5253LL - 103LL * c) + x >= 0LL) && (5151LL - 102LL * c) + x >= 0LL) && (5050LL - 101LL * c) + x >= 0LL) && (4950LL - 100LL * c) + x >= 0LL) && (4851LL - 99LL * c) + x >= 0LL) && (4753LL - 98LL * c) + x >= 0LL) && (4656LL - 97LL * c) + x >= 0LL) && (4560LL - 96LL * c) + x >= 0LL) && (4465LL - 95LL * c) + x >= 0LL) && (4371LL - 94LL * c) + x >= 0LL) && (4278LL - 93LL * c) + x >= 0LL) && (4186LL - 92LL * c) + x >= 0LL) && (4095LL - 91LL * c) + x >= 0LL) && (4005LL - 90LL * c) + x >= 0LL) && (3916LL - 89LL * c) + x >= 0LL) && (3828LL - 88LL * c) + x >= 0LL) && (3741LL - 87LL * c) + x >= 0LL) && (3655LL - 86LL * c) + x >= 0LL) && (3570LL - 85LL * c) + x >= 0LL) && (3486LL - 84LL * c) + x >= 0LL) && (3403LL - 83LL * c) + x >= 0LL) && (3321LL - 82LL * c) + x >= 0LL) && (3240LL - 81LL * c) + x >= 0LL) && (3160LL - 80LL * c) + x >= 0LL) && (3081LL - 79LL * c) + x >= 0LL) && (3003LL - 78LL * c) + x >= 0LL) && (2926LL - 77LL * c) + x >= 0LL) && (2850LL - 76LL * c) + x >= 0LL) && (2775LL - 75LL * c) + x >= 0LL) && (2701LL - 74LL * c) + x >= 0LL) && (2628LL - 73LL * c) + x >= 0LL) && (2556LL - 72LL * c) + x >= 0LL) && (2485LL - 71LL * c) + x >= 0LL) && (2415LL - 70LL * c) + x >= 0LL) && (2346LL - 69LL * c) + x >= 0LL) && (2278LL - 68LL * c) + x >= 0LL) && (2211LL - 67LL * c) + x >= 0LL) && (2145LL - 66LL * c) + x >= 0LL) && (2080LL - 65LL * c) + x >= 0LL) && (2016LL - 64LL * c) + x >= 0LL) && (1953LL - 63LL * c) + x >= 0LL) && (1891LL - 62LL * c) + x >= 0LL) && (1830LL - 61LL * c) + x >= 0LL) && (1770LL - 60LL * c) + x >= 0LL) && (1711LL - 59LL * c) + x >= 0LL) && (1653LL - 58LL * c) + x >= 0LL) && (1596LL - 57LL * c) + x >= 0LL) && (1540LL - 56LL * c) + x >= 0LL) && (1485LL - 55LL * c) + x >= 0LL) && (1431LL - 54LL * c) + x >= 0LL) && (1378LL - 53LL * c) + x >= 0LL) && (1326LL - 52LL * c) + x >= 0LL) && (1275LL - 51LL * c) + x >= 0LL) && (1225LL - 50LL * c) + x >= 0LL) && (1176LL - 49LL * c) + x >= 0LL) && (1128LL - 48LL * c) + x >= 0LL) && (1081LL - 47LL * c) + x >= 0LL) && (1035LL - 46LL * c) + x >= 0LL) && (990LL - 45LL * c) + x >= 0LL) && (946LL - 44LL * c) + x >= 0LL) && (903LL - 43LL * c) + x >= 0LL) && (861LL - 42LL * c) + x >= 0LL) && (820LL - 41LL * c) + x >= 0LL) && (780LL - 40LL * c) + x >= 0LL) && (741LL - 39LL * c) + x >= 0LL) && (703LL - 38LL * c) + x >= 0LL) && (666LL - 37LL * c) + x >= 0LL) && (630LL - 36LL * c) + x >= 0LL) && (595LL - 35LL * c) + x >= 0LL) && (561LL - 34LL * c) + x >= 0LL) && (528LL - 33LL * c) + x >= 0LL) && (496LL - 32LL * c) + x >= 0LL) && (465LL - 31LL * c) + x >= 0LL) && (435LL - 30LL * c) + x >= 0LL) && (406LL - 29LL * c) + x >= 0LL) && (378LL - 28LL * c) + x >= 0LL) && (351LL - 27LL * c) + x >= 0LL) && (325LL - 26LL * c) + x >= 0LL) && (300LL - 25LL * c) + x >= 0LL) && (276LL - 24LL * c) + x >= 0LL) && (253LL - 23LL * c) + x >= 0LL) && (231LL - 22LL * c) + x >= 0LL) && (210LL - 21LL * c) + x >= 0LL) && (190LL - 20LL * c) + x >= 0LL) && (171LL - 19LL * c) + x >= 0LL) && (153LL - 18LL * c) + x >= 0LL) && (136LL - 17LL * c) + x >= 0LL) && (120LL - 16LL * c) + x >= 0LL) && (105LL - 15LL * c) + x >= 0LL) && (91LL - 14LL * c) + x >= 0LL) && (78LL - 13LL * c) + x >= 0LL) && (66LL - 12LL * c) + x >= 0LL) && (55LL - 11LL * c) + x >= 0LL) && (45LL - 10LL * c) + x >= 0LL) && (36LL - 9LL * c) + x >= 0LL) && (28LL - 8LL * c) + x >= 0LL) && (21LL - 7LL * c) + x >= 0LL) && (15LL - 6LL * c) + x >= 0LL) && (10LL - 5LL * c) + x >= 0LL) && (6LL - 4LL * c) + x >= 0LL) && (3LL - 3LL * c) + x >= 0LL) && (1LL - 2LL * c) + x >= 0LL) && (0LL - c) + x >= 0LL) && c >= 0LL) && c <= 32767LL) && 0LL <= c) && 0LL <= x) && 0LL <= y) && (long long )k >= 0LL) && 0 <= (int )k (../plain/ps3-ll_valuebound50.c:35:9-35:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/ps3-ll_valuebound50.c:37:5-37:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/ps3-ll_valuebound50.c:37:5-37:54)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 23
  dead: 0
  total lines: 23
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/ps3-ll_valuebound50.c:27:12-27:13)
[Warning][Witness] invariant unconfirmed: (short)0 <= k (../plain/ps3-ll_valuebound50.c:21:5)
[Warning][Witness] invariant unconfirmed: (long long )k >= 0LL (../plain/ps3-ll_valuebound50.c:21:5)
[Success][Witness] invariant confirmed: 0LL <= y (../plain/ps3-ll_valuebound50.c:27:12)
[Success][Witness] invariant confirmed: 0LL <= x (../plain/ps3-ll_valuebound50.c:27:12)
[Success][Witness] invariant confirmed: 0LL <= c (../plain/ps3-ll_valuebound50.c:27:12)
[Success][Witness] invariant confirmed: c <= 32767LL (../plain/ps3-ll_valuebound50.c:27:12)
[Success][Witness] invariant confirmed: c >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Success][Witness] invariant confirmed: (0LL - c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow
[Warning][Witness] invariant unconfirmed: (1LL - 2LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3LL - 3LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6LL - 4LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (10LL - 5LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (15LL - 6LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (21LL - 7LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (28LL - 8LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (36LL - 9LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (45LL - 10LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (55LL - 11LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (66LL - 12LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (78LL - 13LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (91LL - 14LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (105LL - 15LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (120LL - 16LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (136LL - 17LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (153LL - 18LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (171LL - 19LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (190LL - 20LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (210LL - 21LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (231LL - 22LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (253LL - 23LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (276LL - 24LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (300LL - 25LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (325LL - 26LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (351LL - 27LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (378LL - 28LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (406LL - 29LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (435LL - 30LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (465LL - 31LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (496LL - 32LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (528LL - 33LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (561LL - 34LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (595LL - 35LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (630LL - 36LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (666LL - 37LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (703LL - 38LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (741LL - 39LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (780LL - 40LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (820LL - 41LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (861LL - 42LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (903LL - 43LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (946LL - 44LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (990LL - 45LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1035LL - 46LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1081LL - 47LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1128LL - 48LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1176LL - 49LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1225LL - 50LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1275LL - 51LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1326LL - 52LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1378LL - 53LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1431LL - 54LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1485LL - 55LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1540LL - 56LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1596LL - 57LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1653LL - 58LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1711LL - 59LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1770LL - 60LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1830LL - 61LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1891LL - 62LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (1953LL - 63LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2016LL - 64LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2080LL - 65LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2145LL - 66LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2211LL - 67LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2278LL - 68LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2346LL - 69LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2415LL - 70LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2485LL - 71LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2556LL - 72LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2628LL - 73LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2701LL - 74LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2775LL - 75LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2850LL - 76LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (2926LL - 77LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3003LL - 78LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3081LL - 79LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3160LL - 80LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3240LL - 81LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3321LL - 82LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3403LL - 83LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3486LL - 84LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3570LL - 85LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3655LL - 86LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3741LL - 87LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3828LL - 88LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (3916LL - 89LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4005LL - 90LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4095LL - 91LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4186LL - 92LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4278LL - 93LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4371LL - 94LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4465LL - 95LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4560LL - 96LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4656LL - 97LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4753LL - 98LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4851LL - 99LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (4950LL - 100LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5050LL - 101LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5151LL - 102LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5253LL - 103LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5356LL - 104LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5460LL - 105LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5565LL - 106LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5671LL - 107LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5778LL - 108LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5886LL - 109LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (5995LL - 110LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6105LL - 111LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6216LL - 112LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6328LL - 113LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6441LL - 114LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6555LL - 115LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6670LL - 116LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6786LL - 117LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (6903LL - 118LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (7021LL - 119LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (7140LL - 120LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (7260LL - 121LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (7381LL - 122LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Warning][Witness] invariant unconfirmed: (7503LL - 123LL * c) + x >= 0LL (../plain/ps3-ll_valuebound50.c:27:12)
[Info][Witness] witness validation summary:
  confirmed: 6
  unconfirmed: 124
  refuted: 0
  error: 886
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1016
SV-COMP result: unknown

vars = 45    evals = 89    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            2.021s     2.021s   1229.29MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.11MB      4×
  Cabs2cil                           0.005s     0.005s      4.75MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           1.981s     1.981s   1212.12MB      1×
    createCFG                          0.001s     0.001s      0.63MB      1×
      handle                             0.001s     0.001s      0.10MB     34×
      iter_connect                       0.001s     0.001s      0.42MB     34×
        computeSCCs                        0.001s     0.001s      0.25MB     35×
    FrontC                             0.006s     0.007s      2.30MB    260×
    Cabs2cil                           0.047s     0.047s     25.26MB    260×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.553s     1.554s    411.88MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB     91×
      base unassume                      0.371s     0.371s    348.67MB     13×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.013s     0.013s     10.74MB      1×
        postsolver_iter                    0.013s     0.013s     10.69MB      1×
    warn_global                        0.001s     0.001s      0.13MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
