./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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:5-5516: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.943
[Info] vars: 57008, evals: 50128

[Info] |called|=52

Memory statistics: total=18173.78MB, max=174.57MB, minor=18163.08MB, major=240.56MB, promoted=229.87MB
    minor collections=8668  major collections=15 compactions=0


[Info] runtime: 00:00:21.010
[Info] vars: 85797, evals: 78903

[Info] |called|=28

Memory statistics: total=35585.23MB, max=265.50MB, minor=35570.01MB, major=372.44MB, promoted=357.21MB
    minor collections=16970  major collections=17 compactions=0


[Info] runtime: 00:00:31.098
[Info] vars: 109499, evals: 102601

[Info] |called|=21

Memory statistics: total=52766.48MB, max=305.32MB, minor=52751.04MB, major=485.83MB, promoted=470.39MB
    minor collections=25163  major collections=18 compactions=0

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

[Info] runtime: 00:00:41.125
[Info] vars: 116054, evals: 109156

[Info] |called|=0

Memory statistics: total=70210.21MB, max=351.13MB, minor=70191.28MB, major=624.49MB, promoted=605.56MB
    minor collections=33480  major collections=19 compactions=0


[Info] runtime: 00:00:51.187
[Info] vars: 116054, evals: 109156

[Info] |called|=0

Memory statistics: total=86042.79MB, max=403.80MB, minor=86022.61MB, major=729.49MB, promoted=709.30MB
    minor collections=41029  major collections=20 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5517-5517)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4317
  dead: 1
  total lines: 4318
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4328:18-4328:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1941:18-1941:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1979:21-1979:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3186:19-3186:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1996:21-1996:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4409:20-4409:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2036:18-2036:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2051:19-2051:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3242:18-3242:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2085:18-2085:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3304:19-3304:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4539:21-4539:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:967:19-967:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2162:21-2162:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3448:19-3448:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2253:18-2253:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3455:21-3455:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1080:21-1080:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4657:20-4657:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3469:18-3469:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2288:22-2288:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2295:22-2295:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3502:19-3502:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3522:18-3522:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2402:18-2402:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3581:21-3581:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3636:21-3636:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4844:21-4844:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1294:18-1294:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1300:18-1300:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2482:23-2482:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1307:18-1307:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4880:22-4880:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2530:18-2530:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3708:18-3708:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3715:18-3715:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4961:21-4961:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4975:18-4975:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1425:18-1425:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1443:18-1443:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1449:19-1449:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1476:18-1476:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5046:21-5046:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5061:21-5061:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2681:18-2681:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2689:21-2689:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5078:20-5078:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5095:21-5095:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2709:21-2709:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3924:22-3924:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1571:18-1571:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2753:18-2753:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3946:19-3946:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2800:18-2800:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3995:22-3995:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1630:18-1630:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4015:19-4015:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5211:22-5211:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1644:18-1644:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1650:18-1650:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4056:21-4056:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:4079:21-4079:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5279:18-5279:133)
[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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:118:5-118: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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:143:5-143: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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:168:5-168: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.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:193:5-193:64)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:218:5-218:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1747:24-1747:172)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:243:5-243:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2941:18-2941:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2948:18-2948:155)
[Warning][Deadcode][CWE-571] condition '(int )p7_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:268:5-268:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:2954:21-2954:155)
[Warning][Deadcode][CWE-571] condition '(int )p8_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:293:5-293:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5360:22-5360:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5384:21-5384:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5390:24-5390:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1823:19-1823:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3012:22-3012:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3018:18-3018:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5418:23-5418:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:1872:19-1872:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5467:18-5467:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5483:18-5483:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:3104:18-3104:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.BOUNDED-16.pals+Problem12_label01.c:5507:11-5507:12)
[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)
