./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.UNBOUNDED.pals+Problem12_label09.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.UNBOUNDED.pals+Problem12_label09.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.UNBOUNDED.pals+Problem12_label09.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.UNBOUNDED.pals+Problem12_label09.c:5509:5-5518: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.990
[Info] vars: 57749, evals: 50839

[Info] |called|=24

Memory statistics: total=18400.30MB, max=174.57MB, minor=18389.58MB, major=241.47MB, promoted=230.75MB
    minor collections=8776  major collections=15 compactions=0


[Info] runtime: 00:00:21.074
[Info] vars: 85209, evals: 78287

[Info] |called|=20

Memory statistics: total=34792.51MB, max=230.87MB, minor=34777.29MB, major=364.81MB, promoted=349.59MB
    minor collections=16592  major collections=17 compactions=0


[Info] runtime: 00:00:31.181
[Info] vars: 109364, evals: 102438

[Info] |called|=26

Memory statistics: total=52013.68MB, max=305.32MB, minor=51998.22MB, major=478.52MB, promoted=463.05MB
    minor collections=24804  major collections=18 compactions=0


[Info] runtime: 00:00:41.243
[Info] vars: 116046, evals: 109120

[Info] |called|=0

Memory statistics: total=68316.83MB, max=351.13MB, minor=68297.89MB, major=609.04MB, promoted=590.10MB
    minor collections=32577  major collections=19 compactions=0


[Info] runtime: 00:00:51.318
[Info] vars: 116046, evals: 109120

[Info] |called|=0

Memory statistics: total=85424.34MB, max=403.80MB, minor=85404.12MB, major=723.64MB, promoted=703.42MB
    minor collections=40735  major collections=20 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:676-676)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5519-5519)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4318
  dead: 2
  total lines: 4320
[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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4330:18-4330:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1943:18-1943: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1981:21-1981:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3188:19-3188:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1998:21-1998:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4411:20-4411:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2038:18-2038:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2053:19-2053:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3244:18-3244:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2087:18-2087:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3306:19-3306:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4541:21-4541:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:969:19-969:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2164:21-2164:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3450:19-3450:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2255:18-2255:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3457:21-3457:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1082:21-1082:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4659:20-4659:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3471:18-3471:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2290:22-2290:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2297:22-2297:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3504:19-3504:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3524:18-3524:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2404:18-2404:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3583:21-3583:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3638:21-3638:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4846:21-4846:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1296:18-1296:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1302:18-1302:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2484:23-2484:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1309:18-1309:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4882:22-4882:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2532:18-2532:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3710:18-3710:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3717:18-3717:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4963:21-4963:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4977:18-4977:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1427:18-1427:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1445:18-1445:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1451:19-1451:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1478:18-1478:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5048:21-5048:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5063:21-5063:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2683:18-2683:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2691:21-2691:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5080:20-5080:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5097:21-5097:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2711:21-2711:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3926:22-3926:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1573:18-1573:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2755:18-2755:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3948:19-3948:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2802:18-2802:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3997:22-3997:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1632:18-1632:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4017:19-4017:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5213:22-5213:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1646:18-1646:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1652:18-1652:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4058:21-4058:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:4081:21-4081:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5281:18-5281: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.UNBOUNDED.pals+Problem12_label09.c:121:5-121: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.UNBOUNDED.pals+Problem12_label09.c:146:5-146: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.UNBOUNDED.pals+Problem12_label09.c:171:5-171: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.UNBOUNDED.pals+Problem12_label09.c:196:5-196: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.UNBOUNDED.pals+Problem12_label09.c:221:5-221:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1749:24-1749: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.UNBOUNDED.pals+Problem12_label09.c:246:5-246:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2943:18-2943:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2950:18-2950: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.UNBOUNDED.pals+Problem12_label09.c:271:5-271:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:2956:21-2956: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.UNBOUNDED.pals+Problem12_label09.c:296:5-296:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5362:22-5362:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5386:21-5386:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5392:24-5392:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1825:19-1825:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3014:22-3014:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3020:18-3020:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5420:23-5420: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.UNBOUNDED.pals+Problem12_label09.c:645:10-645:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:1874:19-1874:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5469:18-5469:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:5485:18-5485:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.1.ufo.UNBOUNDED.pals+Problem12_label09.c:3106:18-3106: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.UNBOUNDED.pals+Problem12_label09.c:5509:11-5509: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)
