./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/Problem03_label43.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/Problem03_label43.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/Problem03_label43.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/Problem03_label43.c:1668:5-1678: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 75..80 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:75-80)
  on lines 84..91 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:84-91)
  on lines 157..164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:157-164)
  on lines 166..173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:166-173)
  on lines 202..211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:202-211)
  on lines 213..220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:213-220)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:222-222)
  on lines 377..386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:377-386)
  on lines 388..397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:388-397)
  on lines 399..404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:399-404)
  on line 406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:406-406)
  on lines 469..476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:469-476)
  on lines 721..729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:721-729)
  on lines 824..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:824-834)
  on lines 879..886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:879-886)
  on lines 888..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:888-896)
  on line 898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:898-898)
  on lines 928..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:928-936)
  on lines 938..944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:938-944)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:946-946)
  on lines 958..964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:958-964)
  on lines 1049..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1049-1058)
  on lines 1060..1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1060-1068)
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1070-1070)
  on lines 1085..1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1085-1095)
  on lines 1097..1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1097-1104)
  on lines 1294..1303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1294-1303)
  on lines 1305..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1305-1312)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1314-1314)
  on lines 1370..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1370-1379)
  on lines 1381..1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1381-1388)
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1390-1390)
  on lines 1392..1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1392-1400)
  on lines 1402..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1402-1409)
  on line 1411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1411-1411)
  on lines 1413..1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1413-1420)
  on lines 1422..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1422-1430)
  on line 1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1432-1432)
  on lines 1434..1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1434-1441)
  on lines 1443..1451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1443-1451)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1679-1679)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 1234
  dead: 277
  total lines: 1511
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:223:18-223:244)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1105:20-1105:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1557:17-1557:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1557:17-1557:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1105:20-1105:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:223:18-223:244)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:653:19-653:231)
[Warning][Deadcode][CWE-571] condition 'a4 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:223:18-223:244)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1560:17-1560:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1560:17-1560:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1563:16-1563:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1563:16-1563:101)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:232:19-232:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:663:18-663:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1114:19-1114:230)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:663:18-663:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1114:19-1114:230)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1114:19-1114:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:663:18-663:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1566:17-1566:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1566:17-1566:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:232:19-232:255)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1114:19-1114:230)
[Warning][Deadcode][CWE-571] condition 'a15 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:232:19-232:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1569:16-1569:103)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:668:19-668:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1569:16-1569:103)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1122:19-1122:226)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:668:19-668:232)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:243:24-243:205)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:668:19-668:232)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1572:17-1572:98)
[Warning][Deadcode][CWE-571] condition 'a10 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:668:19-668:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1572:17-1572:98)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1122:19-1122:226)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:668:19-668:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:243:24-243:205)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1122:19-1122:226)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:243:24-243:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:243:24-243:205)
[Warning][Deadcode][CWE-570] condition 'a8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1122:19-1122:226)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1575:16-1575:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1575:16-1575:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:675:18-675:246)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:675:18-675:246)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1578:17-1578:102)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1130:19-1130:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1578:17-1578:102)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1130:19-1130:232)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1130:19-1130:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1130:19-1130:232)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:248:19-248:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:248:19-248:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1581:16-1581:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1581:16-1581:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1584:17-1584:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1584:17-1584:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:685:21-685:259)
[Warning][Deadcode][CWE-570] condition 'a20 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:258:22-258:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:258:22-258:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1137:18-1137:205)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1137:18-1137:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:685:21-685:259)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1137:18-1137:205)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:258:22-258:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:258:22-258:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1587:16-1587:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1587:16-1587:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1137:18-1137:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1590:17-1590:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1590:17-1590:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:267:24-267:253)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:267:24-267:253)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:694:18-694:256)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:694:18-694:256)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:694:18-694:256)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1593:16-1593:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1593:16-1593:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1142:21-1142:328)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:694:18-694:256)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1596:16-1596:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1142:21-1142:328)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1596:16-1596:100)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1142:21-1142:328)
[Warning][Deadcode][CWE-571] condition 'a4 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1142:21-1142:328)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:275:19-275:258)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:275:19-275:258)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1599:16-1599:102)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:275:19-275:258)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1599:16-1599:102)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:275:19-275:258)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:711:19-711:216)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1152:24-1152:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:711:19-711:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1602:17-1602:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1152:24-1152:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1602:17-1602:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1152:24-1152:209)
[Warning][Deadcode][CWE-571] condition '! (a7 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:275:19-275:258)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:711:19-711:216)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:711:19-711:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1605:17-1605:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1605:17-1605:100)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:286:19-286:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:286:19-286:209)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1162:21-1162:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1608:17-1608:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:719:21-719:290)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1608:17-1608:100)
[Warning][Deadcode][CWE-571] condition '! (a23 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:286:19-286:209)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1162:21-1162:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:719:21-719:290)
[Warning][Deadcode][CWE-571] condition '! (a20 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:286:19-286:209)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:286:19-286:209)
[Warning][Deadcode][CWE-571] condition 'a15 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1162:21-1162:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1162:21-1162:208)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1162:21-1162:208)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:719:21-719:290)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1611:16-1611:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1611:16-1611:99)
[Warning][Deadcode][CWE-570] condition 'a11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:720:11-720:18)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:294:20-294:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1614:16-1614:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1614:16-1614:100)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:294:20-294:216)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1172:21-1172:210)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:294:20-294:216)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:294:20-294:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1617:16-1617:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1617:16-1617:101)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1172:21-1172:210)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1172:21-1172:210)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:743:20-743:329)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:743:20-743:329)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1620:16-1620:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1620:16-1620:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:302:18-302:221)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1183:20-1183:236)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1623:17-1623:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1623:17-1623:100)
[Warning][Deadcode][CWE-571] condition '! (a23 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1183:20-1183:236)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:302:18-302:221)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1183:20-1183:236)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:743:20-743:329)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:302:18-302:221)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:743:20-743:329)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1183:20-1183:236)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1626:17-1626:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1626:17-1626:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:311:19-311:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:311:19-311:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1629:16-1629:101)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:311:19-311:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1629:16-1629:101)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:311:19-311:208)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:753:19-753:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:311:19-311:208)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:753:19-753:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:753:19-753:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1192:20-1192:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1632:16-1632:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1632:16-1632:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1192:20-1192:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:753:19-753:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1192:20-1192:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1635:17-1635:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:322:18-322:205)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1635:17-1635:99)
[Warning][Deadcode][CWE-571] condition '! (a8 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:322:18-322:205)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:322:18-322:205)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:322:18-322:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:763:22-763:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:763:22-763:231)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1638:16-1638:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1200:18-1200:204)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1638:16-1638:100)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1200:18-1200:204)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:763:22-763:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1200:18-1200:204)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1641:17-1641:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1641:17-1641:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:329:19-329:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:329:19-329:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1644:17-1644:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1644:17-1644:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1210:18-1210:206)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1210:18-1210:206)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1210:18-1210:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:771:19-771:209)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1210:18-1210:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:771:19-771:209)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1647:16-1647:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1647:16-1647:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:339:18-339:203)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:339:18-339:203)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:339:18-339:203)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1650:17-1650:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1650:17-1650:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1220:18-1220:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1220:18-1220:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1220:18-1220:206)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1220:18-1220:206)
[Warning][Deadcode][CWE-571] condition '! (a10 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1220:18-1220:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:779:22-779:234)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1653:16-1653:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1653:16-1653:101)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:779:22-779:234)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:349:18-349:229)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1656:16-1656:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1656:16-1656:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:349:18-349:229)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:787:18-787:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:787:18-787:255)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1236:18-1236:256)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:787:18-787:255)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1236:18-1236:256)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:358:20-358:255)
[Warning][Deadcode][CWE-570] condition 'a2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:787:18-787:255)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:358:20-358:255)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1236:18-1236:256)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:787:18-787:255)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:358:20-358:255)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:358:20-358:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:358:20-358:255)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:794:22-794:241)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1247:18-1247:290)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:794:22-794:241)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:794:22-794:241)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:794:22-794:241)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition '! (a10 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:794:22-794:241)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1247:18-1247:290)
[Warning][Deadcode][CWE-571] condition '! (a15 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:366:20-366:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1247:18-1247:290)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:366:20-366:209)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:366:20-366:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition 'a0 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1259:19-1259:294)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:376:19-376:243)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1259:19-1259:294)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:805:20-805:239)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1259:19-1259:294)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1668:11-1668:12)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1259:19-1259:294)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1259:19-1259:294)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:814:18-814:242)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:814:18-814:242)
[Warning][Deadcode][CWE-571] condition '! (a19 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:387:20-387:260)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:814:18-814:242)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:387:20-387:260)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1284:18-1284:219)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1284:18-1284:219)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1284:18-1284:219)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:823:20-823:258)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:823:20-823:258)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:407:19-407:242)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1293:19-1293:230)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1293:19-1293:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:835:19-835:246)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:407:19-407:242)
[Warning][Deadcode][CWE-570] condition '! (a0 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:407:19-407:242)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:835:19-835:246)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:835:19-835:246)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:835:19-835:246)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:415:22-415:217)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:415:22-415:217)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:415:22-415:217)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-570] condition '! (a4 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:846:18-846:218)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1315:19-1315:217)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:846:18-846:218)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:846:18-846:218)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:846:18-846:218)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:424:24-424:252)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1323:18-1323:210)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:424:24-424:252)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1323:18-1323:210)
[Warning][Deadcode][CWE-571] condition '! (a23 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1323:18-1323:210)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:424:24-424:252)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1323:18-1323:210)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:854:20-854:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:854:20-854:257)
[Warning][Deadcode][CWE-571] condition '! (a16 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:432:22-432:291)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:432:22-432:291)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1331:19-1331:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:432:22-432:291)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1331:19-1331:205)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1331:19-1331:205)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1331:19-1331:205)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:432:22-432:291)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:863:20-863:243)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:863:20-863:243)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1336:18-1336:244)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1336:18-1336:244)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:444:20-444:231)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:444:20-444:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1336:18-1336:244)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1336:18-1336:244)
[Warning][Deadcode][CWE-570] condition 'a14 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:444:20-444:231)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:873:19-873:206)
[Warning][Deadcode][CWE-570] condition 'a23 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:873:19-873:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:873:19-873:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1346:19-1346:254)
[Warning][Deadcode][CWE-570] condition '! (a0 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:873:19-873:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1346:19-1346:254)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:878:19-878:260)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:451:20-451:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:451:20-451:209)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1354:19-1354:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:460:21-460:233)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1354:19-1354:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:460:21-460:233)
[Warning][Deadcode][CWE-570] condition 'a23 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:899:18-899:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1360:20-1360:244)
[Warning][Deadcode][CWE-570] condition 'a23 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:899:18-899:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:899:18-899:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:899:18-899:206)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1360:20-1360:244)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1360:20-1360:244)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:468:22-468:227)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:468:22-468:227)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:468:22-468:227)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:909:20-909:233)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1369:19-1369:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:909:20-909:233)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:909:20-909:233)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1369:19-1369:230)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:477:20-477:205)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1369:19-1369:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:477:20-477:205)
[Warning][Deadcode][CWE-571] condition 'a4 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:477:20-477:205)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:477:20-477:205)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:477:20-477:205)
[Warning][Deadcode][CWE-570] condition '! (a14 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1369:19-1369:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:917:20-917:254)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:917:20-917:254)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:490:19-490:216)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:490:19-490:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:490:19-490:216)
[Warning][Deadcode][CWE-571] condition 'a10 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1391:18-1391:233)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:490:19-490:216)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1391:18-1391:233)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1391:18-1391:233)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:927:19-927:244)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1391:18-1391:233)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:498:19-498:256)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:498:19-498:256)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:498:19-498:256)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1412:21-1412:232)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1412:21-1412:232)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1412:21-1412:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:947:19-947:332)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:947:19-947:332)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:507:20-507:255)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:507:20-507:255)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:65:14-65:233)
[Warning][Deadcode][CWE-571] condition 'a29 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:507:20-507:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:507:20-507:255)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:507:20-507:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:65:14-65:233)
[Warning][Deadcode][CWE-571] condition '! (a19 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:947:19-947:332)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:947:19-947:332)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1433:18-1433:243)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1433:18-1433:243)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:66:11-66:18)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:957:18-957:258)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:523:20-523:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:523:20-523:216)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:957:18-957:258)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:523:20-523:216)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:83:20-83:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:523:20-523:216)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1442:19-1442:230)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:957:18-957:258)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:83:20-83:231)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:532:25-532:221)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:532:25-532:221)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:532:25-532:221)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:965:19-965:293)
[Warning][Deadcode][CWE-570] condition '! (a16 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:532:25-532:221)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:965:19-965:293)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:92:18-92:255)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:532:25-532:221)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:965:19-965:293)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:92:18-92:255)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1452:20-1452:230)
[Warning][Deadcode][CWE-571] condition 'a10 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:965:19-965:293)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1452:20-1452:230)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1452:20-1452:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:539:20-539:255)
[Warning][Deadcode][CWE-571] condition '! (a8 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:92:18-92:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1452:20-1452:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:539:20-539:255)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1452:20-1452:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:92:18-92:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:976:19-976:257)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:539:20-539:255)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:99:20-99:209)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:976:19-976:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1462:21-1462:211)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1462:21-1462:211)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:976:19-976:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:99:20-99:209)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1462:21-1462:211)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:99:20-99:209)
[Warning][Deadcode][CWE-570] condition '! (a16 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1462:21-1462:211)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:549:19-549:217)
[Warning][Deadcode][CWE-571] condition 'a15 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:549:19-549:217)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:549:19-549:217)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:105:18-105:210)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:549:19-549:217)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:105:18-105:210)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:549:19-549:217)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1470:19-1470:207)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:985:19-985:208)
[Warning][Deadcode][CWE-571] condition 'a15 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1470:19-1470:207)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1470:19-1470:207)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1470:19-1470:207)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:985:19-985:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:556:23-556:229)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:556:23-556:229)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:556:23-556:229)
[Warning][Deadcode][CWE-571] condition 'a16 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:115:20-115:257)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:115:20-115:257)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:993:18-993:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1476:17-1476:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:993:18-993:230)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:115:20-115:257)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1476:17-1476:101)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:115:20-115:257)
[Warning][Deadcode][CWE-571] condition 'a15 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:993:18-993:230)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:993:18-993:230)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:115:20-115:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:993:18-993:230)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1479:17-1479:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1479:17-1479:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1482:16-1482:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1482:16-1482:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:124:21-124:294)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:124:21-124:294)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:566:18-566:332)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:566:18-566:332)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1485:17-1485:99)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:566:18-566:332)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:124:21-124:294)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1485:17-1485:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1004:20-1004:219)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:566:18-566:332)
[Warning][Deadcode][CWE-571] condition '! (a26 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1004:20-1004:219)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1004:20-1004:219)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:124:21-124:294)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:124:21-124:294)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1488:17-1488:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1488:17-1488:100)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:576:19-576:252)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1491:17-1491:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1491:17-1491:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:576:19-576:252)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1013:19-1013:254)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:576:19-576:252)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:576:19-576:252)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1013:19-1013:254)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1013:19-1013:254)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1494:17-1494:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1494:17-1494:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:136:22-136:243)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:136:22-136:243)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:136:22-136:243)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1497:17-1497:98)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1497:17-1497:98)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:584:18-584:231)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1021:18-1021:209)
[Warning][Deadcode][CWE-571] condition 'a23 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:584:18-584:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1021:18-1021:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:145:21-145:241)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:584:18-584:231)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1500:16-1500:102)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1021:18-1021:209)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1500:16-1500:102)
[Warning][Deadcode][CWE-570] condition 'a7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:145:21-145:241)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1503:17-1503:101)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:145:21-145:241)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1503:17-1503:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1031:19-1031:232)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1506:16-1506:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1506:16-1506:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1031:19-1031:232)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1031:19-1031:232)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1031:19-1031:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:593:21-593:243)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:156:20-156:255)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1509:17-1509:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1509:17-1509:101)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1512:16-1512:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1512:16-1512:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1041:21-1041:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:602:19-602:327)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:602:19-602:327)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:602:19-602:327)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:602:19-602:327)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1041:21-1041:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1515:16-1515:100)
[Warning][Deadcode][CWE-571] condition '! (a8 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1041:21-1041:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1515:16-1515:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1041:21-1041:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:165:18-165:233)
[Warning][Deadcode][CWE-571] condition '! (a22 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:165:18-165:233)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:165:18-165:233)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1518:17-1518:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1518:17-1518:100)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1048:20-1048:261)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1521:17-1521:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1521:17-1521:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:613:22-613:252)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1524:16-1524:102)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:613:22-613:252)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1524:16-1524:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:174:20-174:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:174:20-174:257)
[Warning][Deadcode][CWE-570] condition 'a25 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:174:20-174:257)
[Warning][Deadcode][CWE-571] condition '! (a25 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:174:20-174:257)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1527:17-1527:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1527:17-1527:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1071:20-1071:203)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1530:17-1530:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1530:17-1530:100)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1071:20-1071:203)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:182:19-182:259)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1071:20-1071:203)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1071:20-1071:203)
[Warning][Deadcode][CWE-570] condition '! (a22 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1071:20-1071:203)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1533:16-1533:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1533:16-1533:101)
[Warning][Deadcode][CWE-570] condition '! (a22 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:182:19-182:259)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:624:19-624:232)
[Warning][Deadcode][CWE-571] condition 'a22 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:182:19-182:259)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:182:19-182:259)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:624:19-624:232)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:624:19-624:232)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1076:22-1076:206)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1076:22-1076:206)
[Warning][Deadcode][CWE-570] condition '! (a22 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:182:19-182:259)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1536:17-1536:99)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1536:17-1536:99)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1076:22-1076:206)
[Warning][Deadcode][CWE-571] condition '! (a19 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1076:22-1076:206)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1539:16-1539:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1539:16-1539:100)
[Warning][Deadcode][CWE-570] condition '! (a1 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:191:18-191:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:632:19-632:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:191:18-191:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:191:18-191:208)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:632:19-632:208)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:632:19-632:208)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1542:16-1542:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1542:16-1542:102)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1084:22-1084:231)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1545:16-1545:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1545:16-1545:102)
[Warning][Deadcode][CWE-570] condition '! (a5 == 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:201:19-201:241)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1548:17-1548:100)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1548:17-1548:100)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1096:19-1096:232)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:643:19-643:329)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:643:19-643:329)
[Warning][Deadcode][CWE-570] condition 'a17 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:643:19-643:329)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1551:16-1551:101)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1551:16-1551:101)
[Warning][Deadcode][CWE-571] condition 'a1 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:643:19-643:329)
[Warning][Deadcode][CWE-571] condition 'a5 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1554:16-1554:102)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:1554:16-1554:102)
[Warning][Deadcode][CWE-571] condition '! (a17 == 1)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:223:18-223:244)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:653:19-653:231)
[Warning][Deadcode][CWE-571] condition 'a18 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem03_label43.c:223:18-223:244)
[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)
