./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/Problem15_label14.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/Problem15_label14.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/Problem15_label14.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/Problem15_label14.c:1776:5-1785: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 231..234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:231-234)
  on lines 318..321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:318-321)
  on lines 402..405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:402-405)
  on line 537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:537-537)
  on lines 541..543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:541-543)
  on lines 569..570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:569-570)
  on lines 586..589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:586-589)
  on lines 606..608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:606-608)
  on lines 705..708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:705-708)
  on lines 805..806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:805-806)
  on lines 841..843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:841-843)
  on lines 897..898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:897-898)
  on lines 1061..1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1061-1063)
  on lines 1079..1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1079-1081)
  on lines 1146..1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1146-1147)
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1302-1302)
  on lines 1333..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1333-1336)
  on line 1367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1367-1367)
  on lines 1406..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1406-1409)
  on lines 1431..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1431-1433)
  on lines 1454..1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1454-1456)
  on lines 1582..1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1582-1585)
  on lines 1624..1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1624-1625)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1786-1786)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1363
  dead: 67
  total lines: 1430
[Warning][Deadcode][CWE-570] condition '-61 < a0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1430:11-1430:20)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:840:14-840:43)
[Warning][Deadcode][CWE-570] condition '-16 >= a29' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:840:14-840:43)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:224:23-224:173)
[Warning][Deadcode][CWE-571] condition '-147 < a0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1449:14-1449:41)
[Warning][Deadcode][CWE-571] condition '-98 >= a0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1449:14-1449:41)
[Warning][Deadcode][CWE-570] condition 'a0 <= -147' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:230:11-230:23)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:239:19-239:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1466:25-1466:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:865:18-865:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:865:18-865:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1476:18-1476:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:878:21-878:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1483:22-1483:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1488:21-1488:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:895:18-895:172)
[Warning][Deadcode][CWE-571] condition '-147 < a0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:896:14-896:41)
[Warning][Deadcode][CWE-570] condition '-98 >= a0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:896:14-896:41)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1504:18-1504:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1511:21-1511:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:309:21-309:209)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:940:19-940:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:316:18-316:171)
[Warning][Deadcode][CWE-570] condition '43 < a29' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:317:11-317:20)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:945:22-945:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1538:21-1538:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:337:18-337:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:351:22-351:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:351:22-351:192)
[Warning][Deadcode][CWE-571] condition '43 >= a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:352:14-352:41)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:989:19-989:171)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:989:19-989:171)
[Warning][Deadcode][CWE-570] condition 'a2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1581:11-1581:17)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:995:21-995:209)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1599:21-1599:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1008:18-1008:171)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1605:21-1605:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1605:21-1605:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:400:21-400:172)
[Warning][Deadcode][CWE-570] condition 'a2 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:401:11-401:17)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1622:18-1622:172)
[Warning][Deadcode][CWE-570] condition 'a2 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1623:11-1623:17)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:418:18-418:171)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:418:18-418:171)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1633:18-1633:171)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1633:18-1633:171)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:432:21-432:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:449:20-449:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1671:16-1671:165)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1060:14-1060:43)
[Warning][Deadcode][CWE-570] condition '-16 >= a29' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1060:14-1060:43)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1678:19-1678:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1678:19-1678:192)
[Warning][Deadcode][CWE-571] condition 'a2 == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1073:11-1073:17)
[Warning][Deadcode][CWE-570] condition '-98 < a0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1696:14-1696:40)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1711:21-1711:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1716:22-1716:172)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1109:14-1109:41)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1719:21-1719:172)
[Warning][Deadcode][CWE-571] condition '-16 >= a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1720:14-1720:43)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1125:21-1125:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:517:23-517:209)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1745:20-1745:173)
[Warning][Deadcode][CWE-570] condition '-98 < a0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1145:14-1145:40)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1752:19-1752:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1752:19-1752:192)
[Warning][Deadcode][CWE-571] condition 'a0 <= -147' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:531:11-531:23)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:539:19-539:172)
[Warning][Deadcode][CWE-570] condition '-61 < a0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:540:11-540:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1166:18-1166:171)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1166:18-1166:171)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-570] condition 'a2 == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:568:11-568:17)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1182:21-1182:209)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1182:21-1182:209)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-570] condition 'a2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:585:11-585:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1776:11-1776:12)
[Warning][Deadcode][CWE-570] condition '136 < a4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:605:11-605:20)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1222:22-1222:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:630:20-630:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1234:23-1234:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:651:18-651:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:662:20-662:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:667:21-667:173)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1265:22-1265:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1265:22-1265:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:685:20-685:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1287:18-1287:209)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:703:21-703:172)
[Warning][Deadcode][CWE-570] condition 'a4 <= -86' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:704:11-704:22)
[Warning][Deadcode][CWE-570] condition 'a2 == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1300:11-1300:17)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:728:18-728:155)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1331:21-1331:172)
[Warning][Deadcode][CWE-570] condition '-16 < a29' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1332:14-1332:41)
[Warning][Deadcode][CWE-571] condition '43 >= a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1354:21-1354:206)
[Warning][Deadcode][CWE-571] condition 'a0 <= -147' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1361:11-1361:23)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:784:20-784:209)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1381:21-1381:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1381:21-1381:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:789:22-789:172)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:796:22-796:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:796:22-796:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1395:22-1395:192)
[Warning][Deadcode][CWE-571] condition '-16 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1395:22-1395:192)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1398:22-1398:173)
[Warning][Deadcode][CWE-570] condition '-42 < a4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:804:14-804:40)
[Warning][Deadcode][CWE-571] condition '-144 < a29' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1404:22-1404:172)
[Warning][Deadcode][CWE-570] condition 'a0 <= -147' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem15_label14.c:1405:11-1405:23)
[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)
