./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.1.ufo.BOUNDED-8.pals+Problem12_label05.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.1.ufo.BOUNDED-8.pals+Problem12_label05.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.1.ufo.BOUNDED-8.pals+Problem12_label05.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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:332:3-350:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:5-5194: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.970
[Info] vars: 68291, evals: 61466

[Info] |called|=15

Memory statistics: total=20686.68MB, max=200.75MB, minor=20672.64MB, major=254.71MB, promoted=240.67MB
    minor collections=9865  major collections=15 compactions=0


[Info] runtime: 00:00:21.069
[Info] vars: 111002, evals: 104166

[Info] |called|=29

Memory statistics: total=40646.75MB, max=265.50MB, minor=40631.28MB, major=396.43MB, promoted=380.96MB
    minor collections=19383  major collections=17 compactions=0

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

[Info] runtime: 00:00:31.113
[Info] vars: 115676, evals: 108841

[Info] |called|=0

Memory statistics: total=60002.84MB, max=305.32MB, minor=59983.79MB, major=554.58MB, promoted=535.54MB
    minor collections=28612  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5195-5195)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4146
  dead: 1
  total lines: 4147
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2864:19-2864:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1674:21-1674:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4087:20-4087:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1714:18-1714:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1729:19-1729:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2920:18-2920:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1763:18-1763:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2982:19-2982:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4217:21-4217:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:645:19-645:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1840:21-1840:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3126:19-3126:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1931:18-1931:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3133:21-3133:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:758:21-758:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4335:20-4335:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3147:18-3147:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1966:22-1966:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1973:22-1973:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3180:19-3180:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3200:18-3200:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2080:18-2080:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3259:21-3259:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3314:21-3314:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4522:21-4522:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:972:18-972:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:978:18-978:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2160:23-2160:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:985:18-985:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4558:22-4558:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2208:18-2208:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3386:18-3386:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3393:18-3393:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4639:21-4639:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4653:18-4653:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1103:18-1103:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1121:18-1121:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1127:19-1127:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1154:18-1154:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4724:21-4724:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4739:21-4739:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2359:18-2359:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2367:21-2367:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4756:20-4756:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4773:21-4773:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2387:21-2387:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3602:22-3602:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1249:18-1249:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2431:18-2431:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3624:19-3624:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2478:18-2478:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3673:22-3673:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1308:18-1308:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3693:19-3693:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4889:22-4889:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1322:18-1322:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1328:18-1328:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3734:21-3734:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:3757:21-3757:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4957:18-4957:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1425:24-1425:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2619:18-2619:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2626:18-2626:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2632:21-2632:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5038:22-5038: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:87:5-87: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:112:5-112: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:137:5-137: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:162:5-162:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5062:21-5062:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5068:24-5068:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1501:19-1501:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2690:22-2690:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2696:18-2696:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5096:23-5096: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:332:10-332:16)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1550:19-1550:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5145:18-5145:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5161:18-5161:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:2782:18-2782: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:4006:18-4006:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1619:18-1619: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.1.ufo.BOUNDED-8.pals+Problem12_label05.c:5185:11-5185:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.BOUNDED-8.pals+Problem12_label05.c:1657:21-1657: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)
