/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/gj2007.c.i.p+nlh-reducer.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/gj2007.c.i.p+nlh-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/gj2007.c.i.p+nlh-reducer.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: 67 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:422:6)
[Warning][Witness] couldn't locate invariant: main__x <= 99 (../plain/gj2007.c.i.p+nlh-reducer.c:422:6)
[Warning][Witness] couldn't locate invariant: -67LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:422:6)
[Warning][Witness] couldn't locate invariant: 99LL - (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:422:6)
[Warning][Witness] couldn't locate invariant: main__x != 0 (../plain/gj2007.c.i.p+nlh-reducer.c:422:6)
[Warning][Witness] couldn't locate invariant: 67 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: main__x <= 99 (../plain/gj2007.c.i.p+nlh-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: -67LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: 99LL - (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: main__x != 0 (../plain/gj2007.c.i.p+nlh-reducer.c:430:2)
[Warning][Witness] couldn't locate invariant: 67 <= main__y (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 68 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: main__x <= 100 (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: main__y <= 100 (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: -68LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 100LL - (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: main__x != 1 (../plain/gj2007.c.i.p+nlh-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 67 <= main__y (../plain/gj2007.c.i.p+nlh-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: main__y <= 100 (../plain/gj2007.c.i.p+nlh-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: -100LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:439:2)
[Warning][Witness] couldn't locate invariant: -100LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:441:2)
[Warning][Witness] couldn't locate invariant: -100LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:442:6)
[Warning][Witness] couldn't locate invariant: -100LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:449:3)
[Warning][Witness] couldn't locate invariant: -100LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:450:2)
[Info][Witness] unassume invariant: ((((((((-67LL + (long long )main__x >= 0LL && main__y <= 100) && main__x <= 100) && 67 <= main__y) && 67 <= main__x) && -67LL + (long long )main__x >= 0LL) && main__y <= 100) && main__x <= 100) && 67 <= main__y) && 67 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:458:2-458:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/gj2007.c.i.p+nlh-reducer.c:431:2-431:23)
[Info][Witness] unassume invariant: ((((((((-67LL + (long long )main__x >= 0LL && main__y <= 100) && main__x <= 100) && 67 <= main__y) && 67 <= main__x) && -67LL + (long long )main__x >= 0LL) && main__y <= 100) && main__x <= 100) && 67 <= main__y) && 67 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:431:2-431:23)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/gj2007.c.i.p+nlh-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 321 (../plain/gj2007.c.i.p+nlh-reducer.c:321-321)
  on line 327 (../plain/gj2007.c.i.p+nlh-reducer.c:327-327)
  on line 333 (../plain/gj2007.c.i.p+nlh-reducer.c:333-333)
  on line 339 (../plain/gj2007.c.i.p+nlh-reducer.c:339-339)
  on line 345 (../plain/gj2007.c.i.p+nlh-reducer.c:345-345)
  on line 351 (../plain/gj2007.c.i.p+nlh-reducer.c:351-351)
  on line 357 (../plain/gj2007.c.i.p+nlh-reducer.c:357-357)
  on line 363 (../plain/gj2007.c.i.p+nlh-reducer.c:363-363)
  on line 369 (../plain/gj2007.c.i.p+nlh-reducer.c:369-369)
  on line 375 (../plain/gj2007.c.i.p+nlh-reducer.c:375-375)
  on line 381 (../plain/gj2007.c.i.p+nlh-reducer.c:381-381)
  on line 387 (../plain/gj2007.c.i.p+nlh-reducer.c:387-387)
  on line 393 (../plain/gj2007.c.i.p+nlh-reducer.c:393-393)
  on line 399 (../plain/gj2007.c.i.p+nlh-reducer.c:399-399)
  on line 405 (../plain/gj2007.c.i.p+nlh-reducer.c:405-405)
  on line 411 (../plain/gj2007.c.i.p+nlh-reducer.c:411-411)
  on line 417 (../plain/gj2007.c.i.p+nlh-reducer.c:417-417)
  on line 424 (../plain/gj2007.c.i.p+nlh-reducer.c:424-424)
  on line 464 (../plain/gj2007.c.i.p+nlh-reducer.c:464-464)
  on line 476 (../plain/gj2007.c.i.p+nlh-reducer.c:476-476)
  on line 488 (../plain/gj2007.c.i.p+nlh-reducer.c:488-488)
  on line 500 (../plain/gj2007.c.i.p+nlh-reducer.c:500-500)
  on line 512 (../plain/gj2007.c.i.p+nlh-reducer.c:512-512)
  on line 524 (../plain/gj2007.c.i.p+nlh-reducer.c:524-524)
  on line 536 (../plain/gj2007.c.i.p+nlh-reducer.c:536-536)
  on line 548 (../plain/gj2007.c.i.p+nlh-reducer.c:548-548)
  on line 560 (../plain/gj2007.c.i.p+nlh-reducer.c:560-560)
  on line 572 (../plain/gj2007.c.i.p+nlh-reducer.c:572-572)
  on line 584 (../plain/gj2007.c.i.p+nlh-reducer.c:584-584)
  on line 596 (../plain/gj2007.c.i.p+nlh-reducer.c:596-596)
  on line 608 (../plain/gj2007.c.i.p+nlh-reducer.c:608-608)
  on line 620 (../plain/gj2007.c.i.p+nlh-reducer.c:620-620)
  on line 632 (../plain/gj2007.c.i.p+nlh-reducer.c:632-632)
  on line 644 (../plain/gj2007.c.i.p+nlh-reducer.c:644-644)
  on line 656 (../plain/gj2007.c.i.p+nlh-reducer.c:656-656)
  on lines 661..662 (../plain/gj2007.c.i.p+nlh-reducer.c:661-662)
  on line 668 (../plain/gj2007.c.i.p+nlh-reducer.c:668-668)
  on lines 673..674 (../plain/gj2007.c.i.p+nlh-reducer.c:673-674)
  on line 680 (../plain/gj2007.c.i.p+nlh-reducer.c:680-680)
  on lines 685..686 (../plain/gj2007.c.i.p+nlh-reducer.c:685-686)
  on line 692 (../plain/gj2007.c.i.p+nlh-reducer.c:692-692)
  on lines 697..698 (../plain/gj2007.c.i.p+nlh-reducer.c:697-698)
  on line 704 (../plain/gj2007.c.i.p+nlh-reducer.c:704-704)
  on lines 709..710 (../plain/gj2007.c.i.p+nlh-reducer.c:709-710)
  on line 716 (../plain/gj2007.c.i.p+nlh-reducer.c:716-716)
  on lines 721..722 (../plain/gj2007.c.i.p+nlh-reducer.c:721-722)
  on line 728 (../plain/gj2007.c.i.p+nlh-reducer.c:728-728)
  on lines 733..734 (../plain/gj2007.c.i.p+nlh-reducer.c:733-734)
  on line 740 (../plain/gj2007.c.i.p+nlh-reducer.c:740-740)
  on lines 745..746 (../plain/gj2007.c.i.p+nlh-reducer.c:745-746)
  on line 752 (../plain/gj2007.c.i.p+nlh-reducer.c:752-752)
  on lines 757..758 (../plain/gj2007.c.i.p+nlh-reducer.c:757-758)
  on line 764 (../plain/gj2007.c.i.p+nlh-reducer.c:764-764)
  on lines 769..770 (../plain/gj2007.c.i.p+nlh-reducer.c:769-770)
  on line 776 (../plain/gj2007.c.i.p+nlh-reducer.c:776-776)
  on lines 781..782 (../plain/gj2007.c.i.p+nlh-reducer.c:781-782)
  on line 788 (../plain/gj2007.c.i.p+nlh-reducer.c:788-788)
  on lines 793..794 (../plain/gj2007.c.i.p+nlh-reducer.c:793-794)
  on line 800 (../plain/gj2007.c.i.p+nlh-reducer.c:800-800)
  on lines 805..806 (../plain/gj2007.c.i.p+nlh-reducer.c:805-806)
  on line 812 (../plain/gj2007.c.i.p+nlh-reducer.c:812-812)
  on lines 817..818 (../plain/gj2007.c.i.p+nlh-reducer.c:817-818)
  on line 824 (../plain/gj2007.c.i.p+nlh-reducer.c:824-824)
  on lines 829..830 (../plain/gj2007.c.i.p+nlh-reducer.c:829-830)
  on line 836 (../plain/gj2007.c.i.p+nlh-reducer.c:836-836)
  on lines 841..842 (../plain/gj2007.c.i.p+nlh-reducer.c:841-842)
  on line 848 (../plain/gj2007.c.i.p+nlh-reducer.c:848-848)
  on lines 853..854 (../plain/gj2007.c.i.p+nlh-reducer.c:853-854)
  on line 860 (../plain/gj2007.c.i.p+nlh-reducer.c:860-860)
  on lines 865..866 (../plain/gj2007.c.i.p+nlh-reducer.c:865-866)
  on line 872 (../plain/gj2007.c.i.p+nlh-reducer.c:872-872)
  on lines 877..878 (../plain/gj2007.c.i.p+nlh-reducer.c:877-878)
  on line 884 (../plain/gj2007.c.i.p+nlh-reducer.c:884-884)
  on lines 889..890 (../plain/gj2007.c.i.p+nlh-reducer.c:889-890)
  on line 896 (../plain/gj2007.c.i.p+nlh-reducer.c:896-896)
  on lines 901..902 (../plain/gj2007.c.i.p+nlh-reducer.c:901-902)
  on line 908 (../plain/gj2007.c.i.p+nlh-reducer.c:908-908)
  on lines 913..914 (../plain/gj2007.c.i.p+nlh-reducer.c:913-914)
  on line 920 (../plain/gj2007.c.i.p+nlh-reducer.c:920-920)
  on lines 925..926 (../plain/gj2007.c.i.p+nlh-reducer.c:925-926)
  on line 932 (../plain/gj2007.c.i.p+nlh-reducer.c:932-932)
  on lines 937..938 (../plain/gj2007.c.i.p+nlh-reducer.c:937-938)
  on line 944 (../plain/gj2007.c.i.p+nlh-reducer.c:944-944)
  on lines 949..950 (../plain/gj2007.c.i.p+nlh-reducer.c:949-950)
  on line 956 (../plain/gj2007.c.i.p+nlh-reducer.c:956-956)
  on lines 961..962 (../plain/gj2007.c.i.p+nlh-reducer.c:961-962)
  on line 968 (../plain/gj2007.c.i.p+nlh-reducer.c:968-968)
  on lines 973..974 (../plain/gj2007.c.i.p+nlh-reducer.c:973-974)
  on line 980 (../plain/gj2007.c.i.p+nlh-reducer.c:980-980)
  on lines 985..986 (../plain/gj2007.c.i.p+nlh-reducer.c:985-986)
  on line 992 (../plain/gj2007.c.i.p+nlh-reducer.c:992-992)
  on lines 997..998 (../plain/gj2007.c.i.p+nlh-reducer.c:997-998)
  on line 1004 (../plain/gj2007.c.i.p+nlh-reducer.c:1004-1004)
  on lines 1009..1010 (../plain/gj2007.c.i.p+nlh-reducer.c:1009-1010)
  on line 1016 (../plain/gj2007.c.i.p+nlh-reducer.c:1016-1016)
  on lines 1021..1022 (../plain/gj2007.c.i.p+nlh-reducer.c:1021-1022)
  on line 1028 (../plain/gj2007.c.i.p+nlh-reducer.c:1028-1028)
  on lines 1033..1034 (../plain/gj2007.c.i.p+nlh-reducer.c:1033-1034)
  on line 1040 (../plain/gj2007.c.i.p+nlh-reducer.c:1040-1040)
  on lines 1045..1046 (../plain/gj2007.c.i.p+nlh-reducer.c:1045-1046)
  on line 1052 (../plain/gj2007.c.i.p+nlh-reducer.c:1052-1052)
  on lines 1057..1058 (../plain/gj2007.c.i.p+nlh-reducer.c:1057-1058)
  on line 1064 (../plain/gj2007.c.i.p+nlh-reducer.c:1064-1064)
  on lines 1069..1070 (../plain/gj2007.c.i.p+nlh-reducer.c:1069-1070)
  on line 1076 (../plain/gj2007.c.i.p+nlh-reducer.c:1076-1076)
  on lines 1081..1082 (../plain/gj2007.c.i.p+nlh-reducer.c:1081-1082)
  on line 1088 (../plain/gj2007.c.i.p+nlh-reducer.c:1088-1088)
  on lines 1093..1094 (../plain/gj2007.c.i.p+nlh-reducer.c:1093-1094)
  on line 1100 (../plain/gj2007.c.i.p+nlh-reducer.c:1100-1100)
  on lines 1105..1106 (../plain/gj2007.c.i.p+nlh-reducer.c:1105-1106)
  on line 1112 (../plain/gj2007.c.i.p+nlh-reducer.c:1112-1112)
  on lines 1117..1118 (../plain/gj2007.c.i.p+nlh-reducer.c:1117-1118)
  on line 1124 (../plain/gj2007.c.i.p+nlh-reducer.c:1124-1124)
  on lines 1129..1130 (../plain/gj2007.c.i.p+nlh-reducer.c:1129-1130)
  on line 1136 (../plain/gj2007.c.i.p+nlh-reducer.c:1136-1136)
  on lines 1141..1142 (../plain/gj2007.c.i.p+nlh-reducer.c:1141-1142)
  on line 1148 (../plain/gj2007.c.i.p+nlh-reducer.c:1148-1148)
  on lines 1153..1154 (../plain/gj2007.c.i.p+nlh-reducer.c:1153-1154)
  on line 1160 (../plain/gj2007.c.i.p+nlh-reducer.c:1160-1160)
  on lines 1165..1166 (../plain/gj2007.c.i.p+nlh-reducer.c:1165-1166)
  on line 1172 (../plain/gj2007.c.i.p+nlh-reducer.c:1172-1172)
  on lines 1177..1178 (../plain/gj2007.c.i.p+nlh-reducer.c:1177-1178)
  on line 1184 (../plain/gj2007.c.i.p+nlh-reducer.c:1184-1184)
  on lines 1189..1190 (../plain/gj2007.c.i.p+nlh-reducer.c:1189-1190)
  on line 1196 (../plain/gj2007.c.i.p+nlh-reducer.c:1196-1196)
  on lines 1201..1202 (../plain/gj2007.c.i.p+nlh-reducer.c:1201-1202)
  on line 1208 (../plain/gj2007.c.i.p+nlh-reducer.c:1208-1208)
  on lines 1213..1214 (../plain/gj2007.c.i.p+nlh-reducer.c:1213-1214)
  on line 1220 (../plain/gj2007.c.i.p+nlh-reducer.c:1220-1220)
  on lines 1225..1226 (../plain/gj2007.c.i.p+nlh-reducer.c:1225-1226)
  on line 1232 (../plain/gj2007.c.i.p+nlh-reducer.c:1232-1232)
  on lines 1237..1238 (../plain/gj2007.c.i.p+nlh-reducer.c:1237-1238)
  on line 1244 (../plain/gj2007.c.i.p+nlh-reducer.c:1244-1244)
  on lines 1249..1250 (../plain/gj2007.c.i.p+nlh-reducer.c:1249-1250)
  on line 1256 (../plain/gj2007.c.i.p+nlh-reducer.c:1256-1256)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 233
  dead: 187 (2 in uncalled functions)
  total lines: 420
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:341:6-341:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:35:6-35:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:343:6-343:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:37:6-37:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:191:6-191:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:193:6-193:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:347:6-347:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:41:6-41:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:349:6-349:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:43:6-43:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:197:6-197:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:199:6-199:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:353:6-353:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:47:6-47:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:355:6-355:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:49:6-49:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:203:6-203:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:205:6-205:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:359:6-359:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:53:6-53:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:361:6-361:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:55:6-55:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:209:6-209:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:211:6-211:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:365:6-365:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:59:6-59:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:367:6-367:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:61:6-61:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:215:6-215:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:217:6-217:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:371:6-371:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:65:6-65:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:373:6-373:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:67:6-67:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:221:6-221:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:223:6-223:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:377:6-377:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:71:6-71:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:379:6-379:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:73:6-73:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:227:6-227:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:229:6-229:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:383:6-383:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:77:6-77:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:385:6-385:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:79:6-79:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:233:6-233:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:235:6-235:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:389:6-389:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:83:6-83:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:391:6-391:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:85:6-85:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:239:6-239:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:241:6-241:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:395:6-395:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:89:6-89:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:397:6-397:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:91:6-91:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:245:6-245:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:247:6-247:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:401:6-401:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:95:6-95:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:403:6-403:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:97:6-97:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:251:6-251:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:253:6-253:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:407:6-407:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:101:6-101:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:409:6-409:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:103:6-103:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:257:6-257:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:259:6-259:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:413:6-413:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:107:6-107:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:415:6-415:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:109:6-109:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:263:6-263:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:265:6-265:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:113:6-113:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:115:6-115:18)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:422:6-422:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:269:6-269:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:271:6-271:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:119:6-119:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:121:6-121:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:275:6-275:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:277:6-277:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:125:6-125:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:127:6-127:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:281:6-281:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:283:6-283:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:131:6-131:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:133:6-133:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:287:6-287:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:289:6-289:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:137:6-137:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:139:6-139:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:293:6-293:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:295:6-295:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:143:6-143:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:145:6-145:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:299:6-299:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:301:6-301:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:149:6-149:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:151:6-151:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:305:6-305:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:307:6-307:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:155:6-155:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:157:6-157:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:311:6-311:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:313:6-313:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:161:6-161:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:163:6-163:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:317:6-317:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:319:6-319:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:167:6-167:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:169:6-169:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:323:6-323:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:17:6-17:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:325:6-325:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:19:6-19:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:173:6-173:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:175:6-175:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:329:6-329:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:23:6-23:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:331:6-331:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:25:6-25:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:179:6-179:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:181:6-181:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:335:6-335:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:29:6-29:19)
[Warning][Deadcode][CWE-570] condition 'main__x < 50' is always false (../plain/gj2007.c.i.p+nlh-reducer.c:337:6-337:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:31:6-31:18)
[Warning][Deadcode][CWE-571] condition 'main__x < 100' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:185:6-185:19)
[Warning][Deadcode][CWE-571] condition 'main__x < 50' is always true (../plain/gj2007.c.i.p+nlh-reducer.c:187:6-187:18)
[Success][Witness] invariant confirmed: 67 <= main__x (../plain/gj2007.c.i.p+nlh-reducer.c:420:6)
[Success][Witness] invariant confirmed: 67 <= main__y (../plain/gj2007.c.i.p+nlh-reducer.c:420:6)
[Success][Witness] invariant confirmed: main__x <= 100 (../plain/gj2007.c.i.p+nlh-reducer.c:420:6)
[Warning][Witness] invariant unconfirmed: main__y <= 100 (../plain/gj2007.c.i.p+nlh-reducer.c:420:6)
[Success][Witness] invariant confirmed: -67LL + (long long )main__x >= 0LL (../plain/gj2007.c.i.p+nlh-reducer.c:420:6)
[Info][Witness] witness validation summary:
  confirmed: 8
  unconfirmed: 2
  refuted: 0
  error: 24
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 34
SV-COMP result: unknown

vars = 563    evals = 440    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            0.260s     0.261s    215.37MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.89MB      4×
  Cabs2cil                           0.006s     0.006s      6.61MB      4×
  mergeCIL                           0.003s     0.003s      3.55MB      1×
  analysis                           0.217s     0.218s    193.36MB      1×
    createCFG                          0.006s     0.006s      1.97MB      1×
      handle                             0.001s     0.001s      0.53MB     33×
      iter_connect                       0.005s     0.005s      1.25MB     33×
        computeSCCs                        0.004s     0.004s      0.94MB     34×
    FrontC                             0.001s     0.001s      0.12MB     20×
    Cabs2cil                           0.004s     0.004s      1.85MB     20×
    global_inits                       0.001s     0.001s      0.28MB      1×
    solving                            0.182s     0.182s    152.36MB      1×
      S.Dom.equal                        0.001s     0.001s      0.15MB    441×
      base unassume                      0.003s     0.003s      4.33MB      9×
      cheap_full_reach                   0.001s     0.001s      0.16MB      1×
      postsolver                         0.086s     0.086s     73.31MB      1×
        postsolver_iter                    0.085s     0.085s     72.92MB      1×
    warn_global                        0.004s     0.004s      4.35MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
