./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/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.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/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.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/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.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/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:330:3-348:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:5-5192:5 with factor 6
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid

[Info] runtime: 00:00:10.815
[Info] vars: 67783, evals: 60958

[Info] |called|=24

Memory statistics: total=20399.11MB, max=200.75MB, minor=20385.09MB, major=253.05MB, promoted=239.03MB
    minor collections=9728  major collections=15 compactions=0


[Info] runtime: 00:00:20.865
[Info] vars: 110049, evals: 103213

[Info] |called|=26

Memory statistics: total=39975.99MB, max=265.50MB, minor=39960.53MB, major=392.22MB, promoted=376.77MB
    minor collections=19063  major collections=17 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:72:5-72:31)

[Info] runtime: 00:00:30.927
[Info] vars: 115674, evals: 108839

[Info] |called|=0

Memory statistics: total=59631.68MB, max=305.32MB, minor=59612.64MB, major=553.10MB, promoted=534.07MB
    minor collections=28436  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5193-5193)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4145
  dead: 1
  total lines: 4146
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2862:19-2862:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1672:21-1672:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4085:20-4085:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1712:18-1712:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1727:19-1727:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2918:18-2918:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1761:18-1761:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2980:19-2980:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4215:21-4215:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:643:19-643:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1838:21-1838:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3124:19-3124:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1929:18-1929:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3131:21-3131:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:756:21-756:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4333:20-4333:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3145:18-3145:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1964:22-1964:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1971:22-1971:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3178:19-3178:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3198:18-3198:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2078:18-2078:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3257:21-3257:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3312:21-3312:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4520:21-4520:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:970:18-970:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:976:18-976:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2158:23-2158:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:983:18-983:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4556:22-4556:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2206:18-2206:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3384:18-3384:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3391:18-3391:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4637:21-4637:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4651:18-4651:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1101:18-1101:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1119:18-1119:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1125:19-1125:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1152:18-1152:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4722:21-4722:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4737:21-4737:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2357:18-2357:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2365:21-2365:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4754:20-4754:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4771:21-4771:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2385:21-2385:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3600:22-3600:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1247:18-1247:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2429:18-2429:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3622:19-3622:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2476:18-2476:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3671:22-3671:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1306:18-1306:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3691:19-3691:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4887:22-4887:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1320:18-1320:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1326:18-1326:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3732:21-3732:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:3755:21-3755:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4955:18-4955:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1423:24-1423:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2617:18-2617:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2624:18-2624:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2630:21-2630:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5036:22-5036:154)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:85:5-85:64)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:110:5-110:64)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:135:5-135:64)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:160:5-160:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5060:21-5060:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5066:24-5066:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1499:19-1499:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2688:22-2688:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2694:18-2694:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5094:23-5094:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 8' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:330:10-330:16)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1548:19-1548:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5143:18-5143:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5159:18-5159:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:2780:18-2780:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:4004:18-4004:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1617:18-1617:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:5183:11-5183:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.BOUNDED-8.pals+Problem12_label03.c:1655:21-1655:151)
[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)
