./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.4.ufo.UNBOUNDED.pals+Problem12_label06.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.4.ufo.UNBOUNDED.pals+Problem12_label06.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.4.ufo.UNBOUNDED.pals+Problem12_label06.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.4.ufo.UNBOUNDED.pals+Problem12_label06.c:336:3-353:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:5-5197: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.769
[Info] vars: 75673, evals: 68798

[Info] |called|=23

Memory statistics: total=22902.99MB, max=200.75MB, minor=22887.89MB, major=273.72MB, promoted=258.62MB
    minor collections=10921  major collections=15 compactions=0


[Info] runtime: 00:00:20.839
[Info] vars: 115670, evals: 108787

[Info] |called|=0

Memory statistics: total=43540.67MB, max=265.50MB, minor=43523.09MB, major=419.05MB, promoted=401.47MB
    minor collections=20762  major collections=17 compactions=0


[Info] runtime: 00:00:30.882
[Info] vars: 115670, evals: 108787

[Info] |called|=0

Memory statistics: total=64242.00MB, max=351.13MB, minor=64221.86MB, major=584.40MB, promoted=564.26MB
    minor collections=30633  major collections=19 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:355-355)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5198-5198)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4149
  dead: 2
  total lines: 4151
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2867:19-2867:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1677:21-1677:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4090:20-4090:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1717:18-1717:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1732:19-1732:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2923:18-2923:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1766:18-1766:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2985:19-2985:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4220:21-4220:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:648:19-648:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1843:21-1843:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3129:19-3129:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1934:18-1934:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3136:21-3136:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:761:21-761:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4338:20-4338:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3150:18-3150:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1969:22-1969:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1976:22-1976:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3183:19-3183:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3203:18-3203:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2083:18-2083:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3262:21-3262:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3317:21-3317:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4525:21-4525:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:975:18-975:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:981:18-981:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2163:23-2163:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:988:18-988:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4561:22-4561:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2211:18-2211:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3389:18-3389:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3396:18-3396:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4642:21-4642:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4656:18-4656:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1106:18-1106:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1124:18-1124:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1130:19-1130:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1157:18-1157:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4727:21-4727:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4742:21-4742:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2362:18-2362:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2370:21-2370:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4759:20-4759:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4776:21-4776:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2390:21-2390:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3605:22-3605:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1252:18-1252:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2434:18-2434:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3627:19-3627:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2481:18-2481:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3676:22-3676:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1311:18-1311:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3696:19-3696:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4892:22-4892:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1325:18-1325:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1331:18-1331:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3737:21-3737:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:3760:21-3760:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4960:18-4960:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1428:24-1428:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2622:18-2622:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2629:18-2629:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2635:21-2635:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5041:22-5041: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.4.ufo.UNBOUNDED.pals+Problem12_label06.c:91:5-91: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.4.ufo.UNBOUNDED.pals+Problem12_label06.c:116:5-116: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.4.ufo.UNBOUNDED.pals+Problem12_label06.c:141:5-141:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5065:21-5065:154)
[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.4.ufo.UNBOUNDED.pals+Problem12_label06.c:166:5-166:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5071:24-5071:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1504:19-1504:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2693:22-2693:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2699:18-2699:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5099:23-5099:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:336:10-336:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:336:10-336:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1553:19-1553:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5148:18-5148:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5164:18-5164:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:2785:18-2785:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:4009:18-4009:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1622:18-1622:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:5188:11-5188:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.ufo.UNBOUNDED.pals+Problem12_label06.c:1660:21-1660:151)
[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
