./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/Problem17_label57.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/Problem17_label57.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:5-2599:5 with factor 6
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'calculate_output' has dead code:
  on lines 285..288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:285-288)
  on lines 379..381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:379-381)
  on lines 420..423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:420-423)
  on lines 536..539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:536-539)
  on lines 559..562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:559-562)
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:614-614)
  on lines 618..621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:618-621)
  on lines 637..639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:637-639)
  on lines 704..705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:704-705)
  on lines 760..762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:760-762)
  on lines 773..775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:773-775)
  on lines 849..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:849-851)
  on lines 859..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:859-862)
  on lines 931..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:931-933)
  on lines 1028..1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1028-1030)
  on lines 1196..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1196-1198)
  on lines 1232..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1232-1234)
  on lines 1340..1342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1340-1342)
  on lines 1382..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1382-1384)
  on lines 1407..1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1407-1408)
  on lines 1425..1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1425-1427)
  on lines 1440..1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1440-1442)
  on line 1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1557-1557)
  on lines 1586..1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1586-1587)
  on lines 1607..1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1607-1610)
[Warning][Deadcode] Function 'calculate_output2' has dead code:
  on lines 1694..1696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1694-1696)
  on lines 1719..1722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1719-1722)
  on lines 1803..1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1803-1805)
  on lines 1830..1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1830-1832)
  on lines 1873..1875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1873-1875)
  on lines 1918..1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1918-1920)
  on lines 1944..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1944-1947)
  on lines 1975..1978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1975-1978)
  on lines 2032..2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2032-2034)
  on lines 2086..2089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2086-2089)
  on lines 2120..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2120-2121)
  on lines 2197..2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2197-2199)
  on lines 2221..2223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2221-2223)
  on lines 2243..2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2243-2246)
  on lines 2256..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2256-2259)
  on lines 2329..2332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2329-2332)
  on lines 2357..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2357-2359)
  on lines 2401..2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2401-2404)
  on lines 2415..2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2415-2417)
  on lines 2539..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2539-2542)
[Warning][Deadcode] Function 'main' has dead code:
  on line 2600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2600-2600)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 2012
  dead: 144
  total lines: 2156
[Warning][Deadcode][CWE-570] condition '399 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2414:11-2414:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1852:19-1852:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:719:18-719:291)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:179:11-179:109)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1289:22-1289:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2426:22-2426:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:182:11-182:108)
[Warning][Deadcode][CWE-571] condition '-84 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:720:14-720:43)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1855:18-1855:188)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1294:21-1294:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2432:18-2432:188)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:185:11-185:87)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:729:18-729:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1862:18-1862:135)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:188:14-188:148)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1301:21-1301:156)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:729:18-729:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1868:18-1868:133)
[Warning][Deadcode][CWE-571] condition '300 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1869:11-1869:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:191:14-191:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2439:19-2439:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:735:19-735:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1307:21-1307:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1307:21-1307:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:194:14-194:149)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2450:18-2450:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1313:20-1313:116)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1878:19-1878:269)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:197:14-197:147)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1316:18-1316:244)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:747:18-747:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2456:18-2456:209)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1885:24-1885:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:200:14-200:130)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:752:18-752:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1885:24-1885:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1885:24-1885:212)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:752:18-752:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2463:21-2463:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:203:11-203:106)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1323:20-1323:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1891:18-1891:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:206:14-206:128)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:758:20-758:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:758:20-758:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:758:20-758:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1327:24-1327:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2470:25-2470:154)
[Warning][Deadcode][CWE-570] condition 'a14 <= -182' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:759:11-759:24)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:209:11-209:125)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1898:18-1898:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2477:18-2477:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1332:18-1332:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1905:18-1905:192)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:212:11-212:126)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2477:18-2477:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:771:18-771:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:771:18-771:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1338:18-1338:212)
[Warning][Deadcode][CWE-570] condition 'a14 <= -182' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:772:11-772:24)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:215:14-215:126)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2482:18-2482:171)
[Warning][Deadcode][CWE-570] condition '-114 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1339:14-1339:43)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:219:12-219:185)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:781:18-781:175)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1910:21-1910:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2485:19-2485:213)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1349:21-1349:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1916:20-1916:154)
[Warning][Deadcode][CWE-570] condition '399 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1917:11-1917:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:786:24-786:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:225:19-225:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1356:22-1356:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2489:22-2489:138)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1356:22-1356:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1926:19-1926:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:791:21-791:114)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1356:22-1356:231)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1926:19-1926:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:232:18-232:152)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2496:18-2496:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:797:18-797:244)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1362:18-1362:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1932:25-1932:135)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:238:19-238:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1937:18-1937:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2501:27-2501:187)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:241:18-241:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1369:18-1369:171)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:803:21-803:153)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:241:18-241:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2506:21-2506:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1942:21-1942:244)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:810:19-810:231)
[Warning][Deadcode][CWE-570] condition '203 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1943:14-1943:42)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:248:23-248:187)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2512:19-2512:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1374:22-1374:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:248:23-248:187)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:810:19-810:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2512:19-2512:210)
[Warning][Deadcode][CWE-571] condition 'a24 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1375:11-1375:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:253:18-253:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1955:18-1955:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2519:18-2519:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:817:22-817:114)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1955:18-1955:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1387:19-1387:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:824:18-824:157)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2524:22-2524:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1960:18-1960:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:259:21-259:244)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1393:18-1393:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2527:21-2527:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1393:18-1393:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1966:20-1966:172)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:830:21-830:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:830:21-830:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:266:23-266:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1399:18-1399:114)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2532:18-2532:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1973:18-1973:135)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1405:18-1405:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:272:18-272:137)
[Warning][Deadcode][CWE-570] condition 'a28 <= 37' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1974:11-1974:22)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:836:20-836:171)
[Warning][Deadcode][CWE-571] condition '124 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1406:14-1406:42)
[Warning][Deadcode][CWE-570] condition '217 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1406:14-1406:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2537:19-2537:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:841:18-841:172)
[Warning][Deadcode][CWE-570] condition '127 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2538:14-2538:42)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1985:20-1985:210)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1985:20-1985:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:276:26-276:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1985:20-1985:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:847:19-847:135)
[Warning][Deadcode][CWE-570] condition '300 < a28' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:848:11-848:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:283:19-283:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1989:18-1989:188)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1416:18-1416:291)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2549:19-2549:188)
[Warning][Deadcode][CWE-570] condition 'a24 == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:284:11-284:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:857:19-857:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2554:18-2554:231)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2554:18-2554:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1423:19-1423:135)
[Warning][Deadcode][CWE-570] condition 'a24 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1424:11-1424:18)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:857:19-857:210)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2554:18-2554:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1994:19-1994:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:297:20-297:244)
[Warning][Deadcode][CWE-571] condition '124 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:858:14-858:42)
[Warning][Deadcode][CWE-570] condition '217 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:858:14-858:42)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1434:22-1434:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:869:19-869:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1434:22-1434:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2561:19-2561:115)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2001:22-2001:157)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:304:19-304:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1438:18-1438:133)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:304:19-304:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2567:18-2567:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2005:19-2005:244)
[Warning][Deadcode][CWE-570] condition '203 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1439:14-1439:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2567:18-2567:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:875:20-875:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2573:18-2573:223)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:881:20-881:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:881:20-881:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1450:18-1450:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:311:21-311:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:884:18-884:174)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2012:22-2012:187)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1454:22-1454:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2012:22-2012:187)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:316:22-316:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:316:22-316:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2017:21-2017:137)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:890:19-890:231)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1461:21-1461:171)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:890:19-890:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:323:21-323:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2020:20-2020:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1467:22-1467:153)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:329:18-329:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2026:21-2026:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:894:23-894:214)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:329:18-329:155)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:901:18-901:114)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:333:18-333:187)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1472:20-1472:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2030:18-2030:135)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition '-68 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2031:14-2031:42)
[Warning][Deadcode][CWE-570] condition '124 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2031:14-2031:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1477:21-1477:244)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:340:18-340:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:908:18-908:212)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:909:14-909:41)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:340:18-340:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2041:18-2041:291)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:340:18-340:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1484:19-1484:171)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:919:18-919:116)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2590:11-2590:12)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:345:24-345:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:923:19-923:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2048:19-2048:209)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1491:19-1491:212)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2048:19-2048:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1491:19-1491:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:929:18-929:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:352:21-352:244)
[Warning][Deadcode][CWE-570] condition 'a26 <= -68' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:930:11-930:23)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2053:18-2053:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1497:18-1497:135)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2053:18-2053:212)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2053:18-2053:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:357:18-357:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1500:18-1500:291)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:940:20-940:157)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:363:18-363:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2060:21-2060:214)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:363:18-363:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:945:18-945:213)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:370:19-370:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:949:19-949:157)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2067:18-2067:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1507:19-1507:223)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2073:18-2073:172)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:377:22-377:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1514:18-1514:211)
[Warning][Deadcode][CWE-570] condition 'a24 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:378:11-378:18)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1514:18-1514:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:956:19-956:175)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:388:18-388:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2079:18-2079:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:962:18-962:269)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2079:18-2079:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1520:20-1520:152)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2084:19-2084:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:395:21-395:154)
[Warning][Deadcode][CWE-571] condition '-114 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2085:14-2085:43)
[Warning][Deadcode][CWE-570] condition '-84 >= a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2085:14-2085:43)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1525:21-1525:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:402:19-402:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1531:18-1531:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2096:18-2096:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:969:18-969:153)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:402:19-402:209)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:402:19-402:209)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1531:18-1531:231)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:976:22-976:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2102:18-2102:138)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:976:22-976:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:976:22-976:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:409:19-409:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1535:19-1535:152)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2105:22-2105:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2105:22-2105:231)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:982:18-982:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2105:22-2105:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:982:18-982:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:415:18-415:133)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1541:19-1541:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1541:19-1541:210)
[Warning][Deadcode][CWE-571] condition '-84 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:416:11-416:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2111:18-2111:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:985:20-985:156)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2111:18-2111:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:426:18-426:192)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1548:18-1548:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1548:18-1548:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:991:18-991:223)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:426:18-426:192)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2115:18-2115:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2115:18-2115:212)
[Warning][Deadcode][CWE-571] condition 'a24 == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2116:11-2116:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1555:20-1555:135)
[Warning][Deadcode][CWE-571] condition '124 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1556:14-1556:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:433:18-433:136)
[Warning][Deadcode][CWE-570] condition '217 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1556:14-1556:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:438:18-438:152)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1561:22-1561:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:998:21-998:214)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2123:21-2123:137)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1566:19-1566:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:443:19-443:171)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1566:19-1566:231)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1005:22-1005:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1566:19-1566:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1005:22-1005:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1005:22-1005:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2128:19-2128:269)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1573:22-1573:135)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1009:22-1009:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:449:18-449:214)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2135:21-2135:210)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1009:22-1009:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1009:22-1009:212)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2135:21-2135:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:456:20-456:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1580:22-1580:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1015:19-1015:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:456:20-456:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1580:22-1580:174)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1015:19-1015:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2139:21-2139:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1584:18-1584:135)
[Warning][Deadcode][CWE-570] condition 'a28 <= 37' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1585:11-1585:22)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1021:18-1021:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:461:21-461:213)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2145:19-2145:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2145:19-2145:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1592:21-1592:213)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1026:19-1026:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2150:21-2150:155)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1026:19-1026:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1026:19-1026:209)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:468:18-468:212)
[Warning][Deadcode][CWE-570] condition 'a24 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1027:11-1027:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:468:18-468:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2155:19-2155:115)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1597:21-1597:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1038:20-1038:116)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1600:18-1600:137)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2162:18-2162:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:473:18-473:192)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2162:18-2162:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1044:20-1044:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:478:18-478:269)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1605:18-1605:209)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1605:18-1605:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2167:21-2167:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1605:18-1605:209)
[Warning][Deadcode][CWE-570] condition 'a14 <= -182' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1606:11-1606:24)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1050:21-1050:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2173:20-2173:171)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1618:21-1618:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1054:21-1054:133)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:485:22-485:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1623:19-1623:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1060:20-1060:115)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:489:19-489:153)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2178:18-2178:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2178:18-2178:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2178:18-2178:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1066:22-1066:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1630:19-1630:136)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1066:22-1066:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:496:24-496:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:496:24-496:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2182:18-2182:115)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1636:19-1636:212)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1636:19-1636:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:500:18-500:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1073:22-1073:231)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1636:19-1636:212)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1073:22-1073:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2188:18-2188:172)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1073:22-1073:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1642:18-1642:155)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1642:18-1642:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1079:18-1079:213)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2195:18-2195:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1646:18-1646:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:507:21-507:244)
[Warning][Deadcode][CWE-570] condition '203 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2196:14-2196:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1086:18-1086:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1659:11-1659:180)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:512:18-512:223)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2207:19-2207:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:35:14-35:127)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1659:11-1659:180)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1091:21-1091:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:517:18-517:156)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2213:20-2213:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:38:14-38:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1098:18-1098:135)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2213:20-2213:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2213:20-2213:209)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:524:23-524:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:41:11-41:109)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1664:23-1664:244)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:524:23-524:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2219:21-2219:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1104:18-1104:114)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:44:11-44:87)
[Warning][Deadcode][CWE-571] condition '-68 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2220:14-2220:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1669:19-1669:171)
[Warning][Deadcode][CWE-570] condition '124 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2220:14-2220:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:531:18-531:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:47:11-47:105)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1110:21-1110:136)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:531:18-531:231)
[Warning][Deadcode][CWE-571] condition '-114 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:532:14-532:43)
[Warning][Deadcode][CWE-571] condition '-84 >= a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:532:14-532:43)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:50:14-50:107)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2230:19-2230:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1673:21-1673:194)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1116:23-1116:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1116:23-1116:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:53:14-53:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2234:18-2234:269)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:542:20-542:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:56:14-56:107)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1680:19-1680:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1123:26-1123:172)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:545:18-545:194)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:545:18-545:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:59:14-59:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1687:18-1687:188)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2241:18-2241:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:551:19-551:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:62:11-62:108)
[Warning][Deadcode][CWE-571] condition '124 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2242:14-2242:42)
[Warning][Deadcode][CWE-570] condition '217 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2242:14-2242:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1129:21-1129:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:65:11-65:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2254:18-2254:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1135:20-1135:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1692:26-1692:209)
[Warning][Deadcode][CWE-570] condition '203 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1693:14-1693:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:68:14-68:127)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:557:22-557:231)
[Warning][Deadcode][CWE-570] condition '217 < a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2255:11-2255:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:557:22-557:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1140:18-1140:136)
[Warning][Deadcode][CWE-570] condition 'a24 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:558:11-558:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1704:19-1704:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:71:14-71:149)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2266:18-2266:187)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1704:19-1704:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1145:18-1145:173)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:74:11-74:108)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:568:21-568:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:568:21-568:212)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1710:21-1710:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1152:18-1152:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:77:14-77:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2273:23-2273:137)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1710:21-1710:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1155:18-1155:244)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:80:14-80:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2278:21-2278:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1717:18-1717:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:575:19-575:291)
[Warning][Deadcode][CWE-570] condition 'a24 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1718:11-1718:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:83:14-83:147)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:580:21-580:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1728:19-1728:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1162:18-1162:114)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2285:18-2285:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:86:14-86:148)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2285:18-2285:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2285:18-2285:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:586:19-586:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1169:18-1169:171)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:586:19-586:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:89:11-89:105)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2291:19-2291:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2291:19-2291:212)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1733:19-1733:192)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1733:19-1733:192)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:92:11-92:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:592:22-592:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1176:21-1176:156)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2297:18-2297:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1740:22-1740:138)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:95:14-95:148)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:597:22-597:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1182:21-1182:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:98:14-98:109)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1182:21-1182:211)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1745:20-1745:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1745:20-1745:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2303:20-2303:231)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:101:14-101:127)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1189:19-1189:171)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:604:20-604:175)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1751:18-1751:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2307:20-2307:137)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:104:11-104:90)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:609:21-609:136)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:610:11-610:23)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1194:19-1194:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:107:11-107:107)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1194:19-1194:194)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1755:19-1755:154)
[Warning][Deadcode][CWE-570] condition '134 < a28' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1195:14-1195:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2312:18-2312:171)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:616:18-616:116)
[Warning][Deadcode][CWE-570] condition 'a24 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:617:11-617:18)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:110:14-110:109)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2317:18-2317:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:113:11-113:85)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2317:18-2317:211)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1759:18-1759:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1759:18-1759:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1207:24-1207:157)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:628:18-628:192)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:628:18-628:192)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:116:11-116:106)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2323:18-2323:134)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1212:22-1212:214)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1766:20-1766:188)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:635:19-635:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:119:14-119:148)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2327:19-2327:156)
[Warning][Deadcode][CWE-570] condition '399 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:636:11-636:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1773:19-1773:115)
[Warning][Deadcode][CWE-570] condition '-84 < a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2328:11-2328:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:122:11-122:125)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1219:21-1219:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:644:19-644:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1780:18-1780:223)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:125:11-125:109)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2340:19-2340:174)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:644:19-644:211)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2340:19-2340:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:128:14-128:108)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1226:18-1226:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:650:22-650:116)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1787:20-1787:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:131:11-131:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2344:23-2344:175)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1787:20-1787:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1230:18-1230:152)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:657:20-657:212)
[Warning][Deadcode][CWE-571] condition '-182 < a14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1231:14-1231:44)
[Warning][Deadcode][CWE-570] condition '-114 >= a14' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1231:14-1231:44)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:657:20-657:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:134:14-134:108)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2349:18-2349:136)
[Warning][Deadcode][CWE-571] condition '217 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2350:11-2350:21)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1794:21-1794:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1241:19-1241:115)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1794:21-1794:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:137:14-137:127)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1794:21-1794:212)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:663:18-663:210)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:663:18-663:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1247:18-1247:269)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:663:18-663:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:140:11-140:106)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2361:18-2361:213)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1801:19-1801:209)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:143:14-143:129)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1801:19-1801:209)
[Warning][Deadcode][CWE-570] condition '127 < a21' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1802:14-1802:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2368:18-2368:153)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:670:19-670:214)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:146:11-146:107)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1254:19-1254:223)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:149:11-149:88)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1811:23-1811:157)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:677:24-677:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2375:20-2375:152)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:677:24-677:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:677:24-677:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:152:14-152:106)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1817:18-1817:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1259:20-1259:134)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2381:20-2381:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:155:11-155:110)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2381:20-2381:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:683:20-683:175)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1822:22-1822:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:158:11-158:86)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1822:22-1822:174)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:689:21-689:135)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1265:18-1265:291)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:161:11-161:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1828:18-1828:133)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2387:21-2387:244)
[Warning][Deadcode][CWE-571] condition '134 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1829:14-1829:42)
[Warning][Deadcode][CWE-570] condition '300 >= a28' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1829:14-1829:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:696:23-696:154)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:164:14-164:110)
[Warning][Deadcode][CWE-571] condition '-68 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:697:14-697:42)
[Warning][Deadcode][CWE-571] condition '124 >= a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:697:14-697:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2392:19-2392:172)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1841:19-1841:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1272:22-1272:210)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:167:11-167:126)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1841:19-1841:230)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1277:18-1277:155)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2399:22-2399:116)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:708:18-708:133)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:170:14-170:128)
[Warning][Deadcode][CWE-571] condition '37 < a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1277:18-1277:155)
[Warning][Deadcode][CWE-571] condition '124 < a26' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2400:14-2400:42)
[Warning][Deadcode][CWE-570] condition '217 >= a26' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2400:14-2400:42)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1847:18-1847:175)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:173:14-173:128)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1282:18-1282:211)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:713:23-713:212)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:713:23-713:212)
[Warning][Deadcode][CWE-571] condition '300 >= a28' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:1282:18-1282:211)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:176:11-176:89)
[Warning][Deadcode][CWE-571] condition 'a21 <= 127' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem17_label57.c:2413:21-2413:171)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
