./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/Problem10_label42.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/Problem10_label42.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/Problem10_label42.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/Problem10_label42.c:592:5-601: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] function calculate_output uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     reach_error
[Info]   "up":
[Info]     main
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] a1, a10, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, input, input
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'main' has dead code:
  on line 602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:602-602)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 431
  dead: 1
  total lines: 432
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:330:18-330:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:452:19-452:182)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:330:18-330:137)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:196:11-196:74)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:330:18-330:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:196:11-196:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:79:11-79:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:79:11-79:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:458:18-458:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:199:11-199:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:333:21-333:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:199:11-199:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:82:11-82:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:458:18-458:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:82:11-82:91)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:333:21-333:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:202:11-202:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:202:11-202:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:464:19-464:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:85:11-85:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:85:11-85:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:336:19-336:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:464:19-464:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:336:19-336:101)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:205:11-205:91)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:205:11-205:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:88:11-88:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:88:11-88:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:470:18-470:154)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:339:22-339:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:208:11-208:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:208:11-208:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:339:22-339:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:339:22-339:138)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:91:11-91:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:470:18-470:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:91:11-91:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:211:11-211:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:211:11-211:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:94:11-94:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:475:18-475:138)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:94:11-94:91)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:475:18-475:138)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:345:23-345:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:345:23-345:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:475:18-475:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:215:12-215:93)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:215:12-215:93)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:97:11-97:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:97:11-97:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:350:18-350:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:220:18-220:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:220:18-220:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:481:18-481:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:481:18-481:101)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:350:18-350:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:100:11-100:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:100:11-100:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:486:19-486:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:103:11-103:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:225:20-225:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:103:11-103:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:486:19-486:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:355:19-355:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:225:20-225:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:355:19-355:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:106:11-106:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:491:21-491:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:230:18-230:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:106:11-106:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:361:19-361:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:491:21-491:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:230:18-230:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:361:19-361:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:109:11-109:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:109:11-109:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:235:18-235:182)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:364:18-364:138)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:364:18-364:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:497:19-497:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:112:11-112:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:364:18-364:138)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:497:19-497:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:112:11-112:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:235:18-235:182)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:115:11-115:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:115:11-115:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:503:20-503:101)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:241:18-241:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:503:20-503:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:367:19-367:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:241:18-241:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:367:19-367:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:118:11-118:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:118:11-118:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:509:19-509:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:370:18-370:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:370:18-370:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:121:11-121:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:509:19-509:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:246:18-246:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:246:18-246:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:121:11-121:74)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:246:18-246:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:514:19-514:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:124:11-124:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:375:18-375:181)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:124:11-124:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:249:19-249:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:514:19-514:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:249:19-249:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:127:11-127:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:127:11-127:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:375:18-375:181)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:519:18-519:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:130:11-130:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:380:21-380:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:130:11-130:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:519:18-519:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:380:21-380:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:254:19-254:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:254:19-254:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:133:11-133:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:524:19-524:138)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:133:11-133:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:385:18-385:100)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:524:19-524:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:385:18-385:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:259:21-259:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:524:19-524:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:259:21-259:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:136:11-136:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:388:19-388:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:388:19-388:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:136:11-136:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:527:18-527:182)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:527:18-527:182)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:264:19-264:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:139:11-139:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:264:19-264:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:139:11-139:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:393:19-393:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:270:19-270:181)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:142:11-142:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:393:19-393:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:142:11-142:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:533:19-533:137)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:533:19-533:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:533:19-533:137)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:145:11-145:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:398:18-398:181)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:270:19-270:181)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:145:11-145:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:536:18-536:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:536:18-536:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:275:19-275:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:148:11-148:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:148:11-148:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:398:18-398:181)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:31:11-31:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:31:11-31:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:275:19-275:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:151:11-151:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:403:18-403:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:151:11-151:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:539:18-539:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:34:11-34:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:34:11-34:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:403:18-403:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:281:22-281:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:154:11-154:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:539:18-539:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:281:22-281:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:154:11-154:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:37:11-37:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:408:18-408:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:37:11-37:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:544:18-544:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:408:18-408:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:287:18-287:182)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:157:11-157:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:287:18-287:182)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:157:11-157:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:40:11-40:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:40:11-40:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:544:18-544:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:413:19-413:181)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:160:11-160:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:160:11-160:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:43:11-43:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:43:11-43:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:550:18-550:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:413:19-413:181)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:293:19-293:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:163:11-163:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:163:11-163:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:550:18-550:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:46:11-46:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:293:19-293:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:46:11-46:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:418:18-418:137)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:418:18-418:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:296:18-296:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:166:11-166:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:296:18-296:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:418:18-418:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:166:11-166:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:555:18-555:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:555:18-555:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:49:11-49:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:49:11-49:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:169:11-169:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:301:19-301:181)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:169:11-169:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:424:19-424:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:52:11-52:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:424:19-424:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:52:11-52:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:172:11-172:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:558:25-558:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:558:25-558:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:301:19-301:181)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:172:11-172:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:55:11-55:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:429:18-429:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:429:18-429:101)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:55:11-55:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:306:20-306:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:175:11-175:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:564:19-564:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:175:11-175:91)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:564:19-564:137)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:58:11-58:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:564:19-564:137)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:306:20-306:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:58:11-58:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:178:11-178:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:435:22-435:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:178:11-178:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:435:22-435:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:311:19-311:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:567:18-567:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:311:19-311:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:61:11-61:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:61:11-61:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:567:18-567:100)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:181:11-181:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:440:19-440:182)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:181:11-181:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:64:11-64:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:64:11-64:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:573:18-573:154)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:316:21-316:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:184:11-184:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:573:18-573:154)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:316:21-316:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:440:19-440:182)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:67:11-67:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:184:11-184:91)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:67:11-67:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:187:11-187:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:70:11-70:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:579:18-579:120)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:322:18-322:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:187:11-187:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:70:11-70:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:322:18-322:100)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:579:18-579:120)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:446:18-446:132)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:446:18-446:132)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:190:11-190:72)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:73:11-73:91)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:327:19-327:138)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:190:11-190:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:73:11-73:91)
[Warning][Deadcode][CWE-571] condition '-13 < a1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:327:19-327:138)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:592:11-592:12)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:452:19-452:182)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:327:19-327:138)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:193:11-193:74)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:193:11-193:74)
[Warning][Deadcode][CWE-571] condition 'a12 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:76:11-76:72)
[Warning][Deadcode][CWE-571] condition 'a4 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/eca-rers2012/Problem10_label42.c:76:11-76:72)
[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)
