./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/Problem02_label44.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/Problem02_label44.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/Problem02_label44.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/Problem02_label44.c:616:5-626: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 'calculate_output' has dead code:
  on lines 49..51 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:49-51)
  on lines 70..74 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:70-74)
  on lines 94..95 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:94-95)
  on lines 117..122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:117-122)
  on lines 150..152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:150-152)
  on lines 170..174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:170-174)
  on lines 190..194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:190-194)
  on lines 205..207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:205-207)
  on lines 214..216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:214-216)
  on lines 229..232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:229-232)
  on lines 264..268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:264-268)
  on lines 272..277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:272-277)
  on lines 279..283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:279-283)
  on line 285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:285-285)
  on lines 308..310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:308-310)
  on lines 312..316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:312-316)
  on line 318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:318-318)
  on lines 325..330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:325-330)
  on lines 332..335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:332-335)
  on line 337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:337-337)
  on lines 343..344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:343-344)
  on lines 349..350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:349-350)
  on lines 372..377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:372-377)
  on lines 391..393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:391-393)
  on lines 395..396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:395-396)
  on line 398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:398-398)
  on lines 415..416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:415-416)
[Warning][Deadcode] Function 'main' has dead code:
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:627-627)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 401
  dead: 95
  total lines: 496
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:580:15-580:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:347:19-347:153)
[Warning][Deadcode][CWE-570] condition 'a17 == 7' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:348:11-348:18)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:212:21-212:124)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:472:14-472:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:84:17-84:101)
[Warning][Deadcode][CWE-570] condition 'a19 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:85:11-85:18)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:583:15-583:79)
[Warning][Deadcode][CWE-570] condition 'a11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:213:11-213:18)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:475:14-475:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:92:19-92:149)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:586:14-586:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:359:17-359:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:222:18-222:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:478:14-478:79)
[Warning][Deadcode][CWE-570] condition 'a28 == 10' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:93:11-93:19)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:589:14-589:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:364:21-364:125)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:481:14-481:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:101:18-101:100)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:225:17-225:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:592:14-592:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:225:17-225:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:484:14-484:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:371:18-371:99)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:228:21-228:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:595:15-595:78)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:371:18-371:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:105:18-105:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:487:15-487:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:598:15-598:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:378:18-378:124)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:109:18-109:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:490:14-490:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:233:19-233:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:601:14-601:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:493:14-493:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:604:15-604:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:385:18-385:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:235:18-235:153)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:116:19-116:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:496:15-496:79)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:388:19-388:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:242:23-242:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:499:14-499:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:123:18-123:125)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:390:18-390:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:502:15-502:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:244:18-244:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:129:21-129:101)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:505:15-505:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:399:17-399:153)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:247:17-247:153)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:508:14-508:80)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:133:17-133:149)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:511:15-511:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:404:21-404:100)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:258:20-258:125)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:514:15-514:77)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:140:20-140:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:408:19-408:125)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:263:19-263:111)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:517:14-517:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:144:17-144:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:412:19-412:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:520:15-520:77)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:616:11-616:12)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:269:17-269:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:149:19-149:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:414:19-414:99)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:149:19-149:111)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:414:19-414:99)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:149:19-149:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:523:14-523:79)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:271:18-271:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:417:17-417:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:526:14-526:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:153:18-153:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:529:15-529:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:419:18-419:124)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:286:18-286:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:158:18-158:149)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:532:14-532:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:424:14-424:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:290:18-290:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:164:18-164:149)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:535:14-535:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:427:15-427:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:538:15-538:79)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:293:21-293:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:40:12-40:117)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:293:21-293:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:430:15-430:78)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:169:19-169:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:541:15-541:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:45:18-45:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:433:15-433:77)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:544:15-544:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:175:19-175:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:296:18-296:153)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:48:18-48:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:436:15-436:77)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:48:18-48:111)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:48:18-48:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:547:14-547:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:301:18-301:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:439:15-439:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:179:18-179:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:52:18-52:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:550:14-550:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:303:19-303:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:442:14-442:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:185:18-185:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:553:14-553:80)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:57:20-57:113)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:307:18-307:111)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:57:20-57:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:445:14-445:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:189:19-189:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:556:15-556:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:60:18-60:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:448:14-448:78)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:189:19-189:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:559:15-559:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:319:23-319:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:451:15-451:77)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:562:14-562:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:195:19-195:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:64:20-64:149)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:324:18-324:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:454:15-454:79)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:197:18-197:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:565:14-565:80)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:324:18-324:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:457:15-457:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:199:18-199:100)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:568:15-568:77)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:69:18-69:147)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:69:18-69:147)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:460:14-460:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:571:15-571:79)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:201:23-201:113)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:338:19-338:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:201:23-201:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:338:19-338:113)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:463:15-463:80)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:75:18-75:124)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:574:14-574:81)
[Warning][Deadcode][CWE-570] condition 'a17 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:204:18-204:99)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:341:18-341:101)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:466:15-466:79)
[Warning][Deadcode][CWE-570] condition 'a11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:342:11-342:18)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:79:17-79:125)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:577:14-577:81)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:469:15-469:78)
[Warning][Deadcode][CWE-571] condition 'a21 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem02_label44.c:208:17-208:101)
[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
