./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/Problem01_label50.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/Problem01_label50.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/Problem01_label50.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/Problem01_label50.c:593:5-603: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] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'main' has dead code:
  on line 604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:604-604)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 491
  dead: 1
  total lines: 492
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:199:19-199:185)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:431:15-431:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:204:17-204:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:434:15-434:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:207:18-207:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:437:15-437:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:440:16-440:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:443:16-443:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:213:20-213:185)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:446:15-446:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:218:18-218:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:449:15-449:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:224:18-224:122)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:452:16-452:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:228:17-228:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:455:15-455:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:458:16-458:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:233:18-233:110)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:461:16-461:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:241:18-241:160)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:464:15-464:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:467:16-467:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:248:18-248:148)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:470:16-470:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:473:15-473:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:255:18-255:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:476:16-476:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:260:18-260:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:479:16-479:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:266:18-266:122)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:482:15-482:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:485:16-485:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:271:20-271:110)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:488:16-488:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:275:18-275:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:41:12-41:115)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:491:16-491:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:278:19-278:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:45:23-45:160)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:494:15-494:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:283:18-283:148)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:497:16-497:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:53:18-53:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:500:15-500:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:59:18-59:122)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:503:15-503:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:288:23-288:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:506:16-506:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:296:18-296:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:64:19-64:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:509:16-509:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:302:21-302:185)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:512:16-512:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:72:19-72:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:75:19-75:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:515:15-515:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:518:16-518:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:82:18-82:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:309:19-309:185)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:521:15-521:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:524:15-524:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:316:18-316:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:90:20-90:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:527:16-527:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:322:18-322:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:530:16-530:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:326:19-326:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:94:22-94:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:533:16-533:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:328:17-328:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:536:15-536:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:102:18-102:148)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:334:20-334:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:539:15-539:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:107:20-107:185)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:542:16-542:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:339:18-339:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:545:16-545:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:343:18-343:122)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:112:19-112:110)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:548:16-548:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:347:17-347:160)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:118:18-118:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:551:16-551:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:554:16-554:88)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:124:17-124:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:355:18-355:160)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:557:16-557:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:129:18-129:148)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:560:16-560:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:363:18-363:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:563:15-563:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:134:18-134:122)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:365:19-365:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:566:15-566:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:139:19-139:160)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:371:20-371:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:569:16-569:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:373:20-373:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:572:15-572:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:146:19-146:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:375:18-375:110)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:575:15-575:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:150:17-150:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:578:15-578:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:382:19-382:111)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:154:19-154:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:581:15-581:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:387:20-387:110)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:158:18-158:110)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:392:18-392:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:162:20-162:160)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:401:15-401:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:170:18-170:148)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:404:16-404:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:407:15-407:90)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:175:18-175:148)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:410:16-410:89)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:413:15-413:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:183:19-183:185)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:593:11-593:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:416:15-416:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:419:15-419:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:188:22-188:184)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:422:15-422:90)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:196:17-196:112)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:425:16-425:89)
[Warning][Deadcode][CWE-571] condition 'a12 == 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem01_label50.c:428:15-428:89)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
