./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.BOUNDED-6.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.BOUNDED-6.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.BOUNDED-6.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.BOUNDED-6.pals+Problem12_label01.c:266:3-281:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:5116:5-5125: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.884
[Info] vars: 73701, evals: 66887

[Info] |called|=19

Memory statistics: total=20686.10MB, max=200.75MB, minor=20671.00MB, major=256.87MB, promoted=241.77MB
    minor collections=9863  major collections=15 compactions=0

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

[Info] runtime: 00:00:20.941
[Info] vars: 115583, evals: 108761

[Info] |called|=0

Memory statistics: total=41729.17MB, max=265.50MB, minor=41711.26MB, major=416.26MB, promoted=398.35MB
    minor collections=19897  major collections=17 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:5126-5126)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4109
  dead: 1
  total lines: 4110
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1605:21-1605:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4018:20-4018:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1645:18-1645:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1660:19-1660:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2851:18-2851:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1694:18-1694:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2913:19-2913:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4148:21-4148:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:576:19-576:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1771:21-1771:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3057:19-3057:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1862:18-1862:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3064:21-3064:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:689:21-689:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4266:20-4266:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3078:18-3078:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1897:22-1897:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1904:22-1904:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3111:19-3111:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3131:18-3131:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2011:18-2011:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3190:21-3190:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3245:21-3245:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4453:21-4453:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:903:18-903:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:909:18-909:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2091:23-2091:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:916:18-916:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4489:22-4489:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2139:18-2139:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3317:18-3317:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3324:18-3324:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4570:21-4570:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4584:18-4584:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1034:18-1034:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1052:18-1052:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1058:19-1058:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1085:18-1085:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4655:21-4655:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4670:21-4670:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2290:18-2290:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2298:21-2298:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4687:20-4687:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4704:21-4704:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2318:21-2318:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3533:22-3533:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1180:18-1180:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2362:18-2362:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3555:19-3555:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2409:18-2409:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3604:22-3604:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1239:18-1239:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3624:19-3624:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4820:22-4820:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1253:18-1253:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1259:18-1259:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3665:21-3665:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3688:21-3688:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4888:18-4888:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1356:24-1356:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2550:18-2550:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2557:18-2557:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2563:21-2563:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4969:22-4969: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.BOUNDED-6.pals+Problem12_label01.c:80:5-80:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4993:21-4993:154)
[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.BOUNDED-6.pals+Problem12_label01.c:105:5-105:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:4999:24-4999: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.BOUNDED-6.pals+Problem12_label01.c:130:5-130:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1432:19-1432:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2621:22-2621:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2627:18-2627:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:5027:23-5027:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 6' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:266:10-266:16)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1481:19-1481:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:5076:18-5076:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:5092:18-5092:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2713:18-2713: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:3937:18-3937:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1550:18-1550: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.BOUNDED-6.pals+Problem12_label01.c:5116:11-5116:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:1588:21-1588:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c:2795:19-2795: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)
