./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.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.6.ufo.BOUNDED-12.pals+Problem12_label03.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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:477:3-501:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:5-5345: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] cannot unassume entry of type violation_sequence

[Info] runtime: 00:00:10.788
[Info] vars: 64545, evals: 57693

[Info] |called|=28

Memory statistics: total=21136.63MB, max=200.75MB, minor=21125.80MB, major=257.49MB, promoted=246.66MB
    minor collections=10080  major collections=15 compactions=0


[Info] runtime: 00:00:20.897
[Info] vars: 101572, evals: 94706

[Info] |called|=25

Memory statistics: total=40421.05MB, max=265.50MB, minor=40405.69MB, major=398.03MB, promoted=382.67MB
    minor collections=19275  major collections=17 compactions=0

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

[Info] runtime: 00:00:30.943
[Info] vars: 115874, evals: 109008

[Info] |called|=0

Memory statistics: total=59302.38MB, max=305.32MB, minor=59283.50MB, major=544.14MB, promoted=525.26MB
    minor collections=28278  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5346-5346)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4228
  dead: 1
  total lines: 4229
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1808:21-1808:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3015:19-3015:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1825:21-1825:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4238:20-4238:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1865:18-1865:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1880:19-1880:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3071:18-3071:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1914:18-1914:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3133:19-3133:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4368:21-4368:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:796:19-796:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1991:21-1991:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3277:19-3277:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2082:18-2082:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3284:21-3284:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:909:21-909:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4486:20-4486:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3298:18-3298:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2117:22-2117:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2124:22-2124:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3331:19-3331:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3351:18-3351:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2231:18-2231:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3410:21-3410:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3465:21-3465:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4673:21-4673:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1123:18-1123:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1129:18-1129:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2311:23-2311:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1136:18-1136:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4709:22-4709:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2359:18-2359:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3537:18-3537:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3544:18-3544:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4790:21-4790:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4804:18-4804:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1254:18-1254:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1272:18-1272:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1278:19-1278:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1305:18-1305:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4875:21-4875:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4890:21-4890:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2510:18-2510:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2518:21-2518:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4907:20-4907:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4924:21-4924:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2538:21-2538:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3753:22-3753:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1400:18-1400:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2582:18-2582:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3775:19-3775:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2629:18-2629:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3824:22-3824:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1459:18-1459:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3844:19-3844:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5040:22-5040:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1473:18-1473:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1479:18-1479:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3885:21-3885:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:3908:21-3908:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5108:18-5108: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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:102:5-102:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1576:24-1576:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2770:18-2770:155)
[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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:127:5-127:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2777:18-2777:155)
[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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:152:5-152:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2783:21-2783:155)
[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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:177:5-177: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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:202:5-202:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5189:22-5189:154)
[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.6.ufo.BOUNDED-12.pals+Problem12_label03.c:227:5-227:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5213:21-5213:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5219:24-5219:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1652:19-1652:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2841:22-2841:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2847:18-2847:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5247:23-5247:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 12' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:477:10-477:17)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1701:19-1701:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5296:18-5296:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5312:18-5312:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:2933:18-2933:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:5336:11-5336:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:4157:18-4157:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.BOUNDED-12.pals+Problem12_label03.c:1770:18-1770:154)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
