./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/Problem11_label31.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/Problem11_label31.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/Problem11_label31.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/Problem11_label31.c:1044:5-1053:5 with factor 6
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'calculate_output' has dead code:
  on lines 410..413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:410-413)
  on lines 499..501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:499-501)
  on lines 526..529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:526-529)
  on lines 604..605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:604-605)
  on lines 621..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:621-622)
  on lines 663..665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:663-665)
  on lines 710..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:710-713)
  on lines 729..732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:729-732)
  on lines 769..772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:769-772)
  on lines 820..823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:820-823)
  on lines 877..879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:877-879)
  on lines 915..916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:915-916)
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:934-934)
  on lines 951..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:951-954)
  on lines 981..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:981-982)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1054-1054)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 740
  dead: 47
  total lines: 787
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:401:21-401:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:991:18-991:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:698:20-698:152)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:401:21-401:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:165:15-165:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:698:20-698:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:165:15-165:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:408:18-408:140)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:408:18-408:140)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:704:17-704:170)
[Warning][Deadcode][CWE-570] condition '140 < a29' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:409:14-409:42)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:168:15-168:130)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:168:15-168:130)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:998:27-998:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:998:27-998:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:704:17-704:170)
[Warning][Deadcode][CWE-571] condition 'a23 <= -43' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:705:11-705:23)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:171:15-171:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1003:19-1003:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:421:18-421:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:171:15-171:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1003:19-1003:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:421:18-421:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:174:15-174:111)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:174:15-174:111)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1010:18-1010:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1010:18-1010:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:716:27-716:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:716:27-716:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:427:21-427:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:427:21-427:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:177:12-177:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:177:12-177:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:722:18-722:146)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1015:18-1015:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1015:18-1015:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:722:18-722:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:432:18-432:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:180:12-180:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:180:12-180:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:432:18-432:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:727:20-727:120)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:183:12-183:111)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1022:19-1022:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:183:12-183:111)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:727:20-727:120)
[Warning][Deadcode][CWE-570] condition 'a25 == 9' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:728:11-728:18)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1022:19-1022:146)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:186:12-186:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:439:22-439:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:439:22-439:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:186:12-186:93)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:741:18-741:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1027:18-1027:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1027:18-1027:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:189:12-189:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:189:12-189:110)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:446:18-446:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:741:18-741:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:446:18-446:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:192:12-192:90)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:192:12-192:90)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:748:18-748:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:453:18-453:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:195:12-195:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:453:18-453:170)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:195:12-195:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:748:18-748:149)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:198:15-198:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:198:15-198:112)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:460:20-460:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:460:20-460:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:201:15-201:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:753:21-753:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:753:21-753:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:201:15-201:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:466:21-466:141)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:760:18-760:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:466:21-466:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:204:15-204:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:204:15-204:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:760:18-760:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:473:18-473:245)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:207:15-207:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:207:15-207:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:767:21-767:120)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:767:21-767:120)
[Warning][Deadcode][CWE-570] condition 'a8 == 17' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:768:11-768:18)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:210:12-210:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:210:12-210:112)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:473:18-473:245)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:779:18-779:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:779:18-779:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:213:15-213:111)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:213:15-213:111)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:1044:11-1044:12)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:217:15-217:134)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:217:15-217:134)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:784:17-784:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:480:20-480:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:480:20-480:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:784:17-784:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:224:17-224:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:790:18-790:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:487:18-487:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:487:18-487:141)
[Warning][Deadcode][CWE-570] condition 'a8 == 17' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:488:11-488:18)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:33:12-33:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:33:12-33:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:224:17-224:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:790:18-790:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:497:19-497:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:36:15-36:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:36:15-36:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:231:18-231:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:231:18-231:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:497:19-497:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:797:24-797:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:797:24-797:140)
[Warning][Deadcode][CWE-570] condition 'a8 == 16' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:498:11-498:18)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:39:12-39:109)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:39:12-39:109)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:237:20-237:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:802:19-802:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:802:19-802:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:237:20-237:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:42:12-42:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:510:18-510:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:42:12-42:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:510:18-510:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:243:19-243:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:809:18-809:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:809:18-809:243)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:45:12-45:111)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:45:12-45:111)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:243:19-243:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:48:15-48:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:48:15-48:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:517:19-517:171)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:517:19-517:171)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:814:21-814:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:51:12-51:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:51:12-51:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:814:21-814:225)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:815:11-815:18)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:54:12-54:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:250:20-250:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:250:20-250:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:524:19-524:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:54:12-54:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:524:19-524:152)
[Warning][Deadcode][CWE-571] condition '138 < a23' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:525:14-525:42)
[Warning][Deadcode][CWE-570] condition '306 >= a23' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:525:14-525:42)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:257:19-257:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:57:12-57:91)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:57:12-57:91)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:536:18-536:149)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:257:19-257:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:60:15-60:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:826:23-826:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:826:23-826:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:536:18-536:149)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:60:15-60:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:264:23-264:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:63:12-63:90)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:264:23-264:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:541:24-541:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:63:12-63:90)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:541:24-541:140)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:832:18-832:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:832:18-832:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:66:12-66:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:835:18-835:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:66:12-66:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:835:18-835:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:547:18-547:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:547:18-547:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:69:12-69:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:270:20-270:243)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:270:20-270:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:69:12-69:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:841:21-841:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:552:20-552:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:275:19-275:120)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:841:21-841:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:552:20-552:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:72:15-72:130)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:275:19-275:120)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:72:15-72:130)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:846:19-846:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:846:19-846:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:559:20-559:170)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:278:18-278:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:278:18-278:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:75:15-75:130)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:75:15-75:130)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:559:20-559:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:851:19-851:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:78:12-78:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:851:19-851:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:285:19-285:152)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:565:18-565:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:285:19-285:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:78:12-78:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:565:18-565:171)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:856:17-856:120)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:856:17-856:120)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:81:15-81:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:81:15-81:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:290:18-290:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:571:18-571:146)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:862:18-862:245)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:84:15-84:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:571:18-571:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:84:15-84:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:290:18-290:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:576:17-576:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:87:12-87:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:87:12-87:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:862:18-862:245)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:297:18-297:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:576:17-576:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:297:18-297:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:90:15-90:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:869:18-869:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:869:18-869:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:90:15-90:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:582:18-582:120)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:582:18-582:120)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:304:18-304:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:304:18-304:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:93:15-93:130)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:93:15-93:130)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:585:23-585:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:585:23-585:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:875:25-875:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:875:25-875:171)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:309:18-309:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:309:18-309:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:96:12-96:92)
[Warning][Deadcode][CWE-570] condition 'a4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:876:11-876:17)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:96:12-96:92)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:591:18-591:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:591:18-591:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:99:15-99:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:99:15-99:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:315:20-315:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:886:22-886:150)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:886:22-886:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:315:20-315:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:596:22-596:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:102:15-102:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:102:15-102:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:891:20-891:243)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:320:18-320:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:320:18-320:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:596:22-596:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:597:11-597:17)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:105:12-105:93)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:105:12-105:93)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:891:20-891:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:327:20-327:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:608:20-608:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:108:15-108:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:108:15-108:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:608:20-608:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:327:20-327:168)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:896:19-896:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:896:19-896:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:111:15-111:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:332:19-332:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:111:15-111:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:613:18-613:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:332:19-332:152)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:903:20-903:149)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:613:18-613:149)
[Warning][Deadcode][CWE-571] condition 'a4 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:614:11-614:17)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:114:15-114:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:903:20-903:149)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:114:15-114:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:339:20-339:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:908:21-908:146)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:625:22-625:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:339:20-339:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:117:12-117:91)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:117:12-117:91)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:908:21-908:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:625:22-625:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:120:15-120:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:344:18-344:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:913:19-913:225)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:120:15-120:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:913:19-913:225)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:631:20-631:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:344:18-344:170)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:631:20-631:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:123:15-123:131)
[Warning][Deadcode][CWE-570] condition 'a8 == 16' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:914:11-914:18)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:123:15-123:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:638:20-638:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:638:20-638:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:126:12-126:109)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:925:21-925:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:350:25-350:225)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:126:12-126:109)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:350:25-350:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:925:21-925:152)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:926:11-926:17)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:129:12-129:91)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:645:23-645:152)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:129:12-129:91)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:645:23-645:152)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:356:17-356:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:356:17-356:137)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:132:15-132:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:937:20-937:120)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:937:20-937:120)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:132:15-132:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:652:18-652:146)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:363:18-363:243)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:363:18-363:243)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:942:19-942:246)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:652:18-652:146)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:135:15-135:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:135:15-135:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:942:19-942:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:657:25-657:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:138:12-138:110)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:657:25-657:171)
[Warning][Deadcode][CWE-571] condition '-43 < a23' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:658:14-658:42)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:138:12-138:110)
[Warning][Deadcode][CWE-571] condition '138 >= a23' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:658:14-658:42)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:949:19-949:150)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:141:15-141:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:141:15-141:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:949:19-949:150)
[Warning][Deadcode][CWE-570] condition 'a29 <= 140' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:950:11-950:23)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:368:20-368:245)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:368:20-368:245)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:668:19-668:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:668:19-668:171)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:144:12-144:91)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:144:12-144:91)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:963:18-963:140)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:673:18-673:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:963:18-963:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:375:18-375:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:375:18-375:168)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:147:12-147:112)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:673:18-673:140)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:147:12-147:112)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:968:18-968:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:150:12-150:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:680:17-680:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:380:21-380:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:380:21-380:141)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:150:12-150:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:968:18-968:153)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:153:12-153:110)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:680:17-680:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:973:19-973:119)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:153:12-153:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:387:22-387:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:973:19-973:119)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:685:19-685:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:156:15-156:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:387:22-387:246)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:156:15-156:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:685:19-685:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:979:19-979:225)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:159:15-159:131)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:979:19-979:225)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:394:18-394:137)
[Warning][Deadcode][CWE-570] condition 'a4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:980:11-980:17)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:159:15-159:131)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:394:18-394:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:691:18-691:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:691:18-691:141)
[Warning][Deadcode][CWE-571] condition 'a3 == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:162:12-162:110)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:991:18-991:137)
[Warning][Deadcode][CWE-571] condition 'a8 == 15' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem11_label31.c:162:12-162:110)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
