./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.5.ufo.BOUNDED-10.pals+Problem12_label07.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.5.ufo.BOUNDED-10.pals+Problem12_label07.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.5.ufo.BOUNDED-10.pals+Problem12_label07.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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:403:3-424:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:5-5268: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.856
[Info] vars: 66447, evals: 59606

[Info] |called|=83

Memory statistics: total=21184.40MB, max=200.75MB, minor=21170.40MB, major=259.73MB, promoted=245.73MB
    minor collections=10102  major collections=15 compactions=0


[Info] runtime: 00:00:20.941
[Info] vars: 107629, evals: 100778

[Info] |called|=19

Memory statistics: total=41805.23MB, max=265.50MB, minor=41789.80MB, major=403.78MB, promoted=388.36MB
    minor collections=19935  major collections=17 compactions=0

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

[Info] runtime: 00:00:31.016
[Info] vars: 115775, evals: 108924

[Info] |called|=0

Memory statistics: total=62664.52MB, max=305.32MB, minor=62645.50MB, major=570.91MB, promoted=551.89MB
    minor collections=29882  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5269-5269)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4187
  dead: 1
  total lines: 4188
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1731:21-1731:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2938:19-2938:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1748:21-1748:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4161:20-4161:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1788:18-1788:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1803:19-1803:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2994:18-2994:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1837:18-1837:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3056:19-3056:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4291:21-4291:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:719:19-719:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1914:21-1914:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3200:19-3200:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2005:18-2005:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3207:21-3207:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:832:21-832:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4409:20-4409:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3221:18-3221:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2040:22-2040:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2047:22-2047:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3254:19-3254:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3274:18-3274:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2154:18-2154:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3333:21-3333:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3388:21-3388:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4596:21-4596:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1046:18-1046:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1052:18-1052:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2234:23-2234:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1059:18-1059:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4632:22-4632:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2282:18-2282:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3460:18-3460:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3467:18-3467:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4713:21-4713:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4727:18-4727:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1177:18-1177:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1195:18-1195:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1201:19-1201:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1228:18-1228:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4798:21-4798:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4813:21-4813:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2433:18-2433:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2441:21-2441:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4830:20-4830:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4847:21-4847:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2461:21-2461:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3676:22-3676:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1323:18-1323:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2505:18-2505:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3698:19-3698:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2552:18-2552:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3747:22-3747:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1382:18-1382:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3767:19-3767:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4963:22-4963:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1396:18-1396:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1402:18-1402:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3808:21-3808:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:3831:21-3831:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5031:18-5031:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1499:24-1499:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2693:18-2693:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2700:18-2700:155)
[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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:95:5-95:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2706:21-2706: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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:120:5-120:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5112:22-5112: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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:145:5-145: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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:170:5-170: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.5.ufo.BOUNDED-10.pals+Problem12_label07.c:195:5-195:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5136:21-5136:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5142:24-5142:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1575:19-1575:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2764:22-2764:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2770:18-2770:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5170:23-5170:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:403:10-403:17)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1624:19-1624:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5219:18-5219:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5235:18-5235:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:2856:18-2856:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:4080:18-4080:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:1693:18-1693:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.ufo.BOUNDED-10.pals+Problem12_label07.c:5259:11-5259:12)
[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
