./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.3.1.ufo.UNBOUNDED.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.3.1.ufo.UNBOUNDED.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.3.1.ufo.UNBOUNDED.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.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:272:3-286:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:5-5130: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.832
[Info] vars: 74834, evals: 67980

[Info] |called|=26

Memory statistics: total=20728.18MB, max=200.75MB, minor=20713.07MB, major=258.05MB, promoted=242.94MB
    minor collections=9885  major collections=15 compactions=0


[Info] runtime: 00:00:20.899
[Info] vars: 115592, evals: 108730

[Info] |called|=0

Memory statistics: total=41431.64MB, max=265.50MB, minor=41413.74MB, major=415.15MB, promoted=397.25MB
    minor collections=19757  major collections=17 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:288-288)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5131-5131)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4113
  dead: 2
  total lines: 4115
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2800:19-2800:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1610:21-1610:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4023:20-4023:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1650:18-1650:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1665:19-1665:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2856:18-2856:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1699:18-1699:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2918:19-2918:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4153:21-4153:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:581:19-581:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1776:21-1776:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3062:19-3062:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1867:18-1867:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3069:21-3069:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:694:21-694:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4271:20-4271:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3083:18-3083:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1902:22-1902:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1909:22-1909:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3116:19-3116:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3136:18-3136:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2016:18-2016:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3195:21-3195:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3250:21-3250:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4458:21-4458:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:908:18-908:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:914:18-914:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2096:23-2096:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:921:18-921:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4494:22-4494:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2144:18-2144:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3322:18-3322:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3329:18-3329:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4575:21-4575:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4589:18-4589:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1039:18-1039:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1057:18-1057:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1063:19-1063:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1090:18-1090:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4660:21-4660:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4675:21-4675:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2295:18-2295:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2303:21-2303:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4692:20-4692:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4709:21-4709:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2323:21-2323:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3538:22-3538:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1185:18-1185:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2367:18-2367:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3560:19-3560:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2414:18-2414:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3609:22-3609:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1244:18-1244:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3629:19-3629:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4825:22-4825:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1258:18-1258:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1264:18-1264:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3670:21-3670:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3693:21-3693:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4893:18-4893:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1361:24-1361:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2555:18-2555:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2562:18-2562:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2568:21-2568:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4974:22-4974: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.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:86:5-86: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.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:111:5-111:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:4998:21-4998:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5004:24-5004:154)
[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.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:136:5-136:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1437:19-1437:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2626:22-2626:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2632:18-2632:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5032:23-5032:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:272:10-272:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:272:10-272:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:272:10-272:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1486:19-1486:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5081:18-5081:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5097:18-5097:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:2718:18-2718:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:3942:18-3942:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1555:18-1555:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:5121:11-5121:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c:1593:21-1593: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)
