./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.7.ufo.BOUNDED-14.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.7.ufo.BOUNDED-14.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.7.ufo.BOUNDED-14.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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:555:3-582:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:5-5426: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.866
[Info] vars: 61176, evals: 54309

[Info] |called|=21

Memory statistics: total=19906.29MB, max=200.75MB, minor=19895.52MB, major=250.67MB, promoted=239.91MB
    minor collections=9494  major collections=15 compactions=0


[Info] runtime: 00:00:20.957
[Info] vars: 96318, evals: 89437

[Info] |called|=79

Memory statistics: total=39472.88MB, max=265.50MB, minor=39457.59MB, major=395.86MB, promoted=380.57MB
    minor collections=18824  major collections=17 compactions=0

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

[Info] runtime: 00:00:31.006
[Info] vars: 115976, evals: 109094

[Info] |called|=0

Memory statistics: total=59799.22MB, max=305.32MB, minor=59780.91MB, major=545.92MB, promoted=527.62MB
    minor collections=28516  major collections=19 compactions=0


[Info] runtime: 00:00:41.048
[Info] vars: 115976, evals: 109094

[Info] |called|=0

Memory statistics: total=79254.58MB, max=351.13MB, minor=79235.47MB, major=682.49MB, promoted=663.38MB
    minor collections=37793  major collections=20 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5427-5427)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4271
  dead: 1
  total lines: 4272
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4238:18-4238:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1851:18-1851:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1889:21-1889:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3096:19-3096:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1906:21-1906:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4319:20-4319:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1946:18-1946:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1961:19-1961:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3152:18-3152:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1995:18-1995:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3214:19-3214:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4449:21-4449:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:877:19-877:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2072:21-2072:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3358:19-3358:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2163:18-2163:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3365:21-3365:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:990:21-990:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4567:20-4567:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3379:18-3379:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2198:22-2198:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2205:22-2205:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3412:19-3412:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3432:18-3432:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2312:18-2312:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3491:21-3491:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3546:21-3546:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4754:21-4754:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1204:18-1204:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1210:18-1210:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2392:23-2392:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1217:18-1217:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4790:22-4790:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2440:18-2440:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3618:18-3618:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3625:18-3625:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4871:21-4871:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4885:18-4885:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1335:18-1335:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1353:18-1353:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1359:19-1359:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1386:18-1386:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4956:21-4956:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4971:21-4971:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2591:18-2591:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2599:21-2599:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:4988:20-4988:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5005:21-5005:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2619:21-2619:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3834:22-3834:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1481:18-1481:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2663:18-2663:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3856:19-3856:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2710:18-2710:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3905:22-3905:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1540:18-1540:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3925:19-3925:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5121:22-5121:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1554:18-1554:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1560:18-1560:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3966:21-3966:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3989:21-3989:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5189:18-5189: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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:109:5-109: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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:134:5-134: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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:159:5-159:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1657:24-1657:172)
[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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:184:5-184:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2851:18-2851:155)
[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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:209:5-209:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2858:18-2858:155)
[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.7.ufo.BOUNDED-14.pals+Problem12_label07.c:234:5-234:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2864:21-2864:155)
[Warning][Deadcode][CWE-571] condition '(int )p7_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:259:5-259:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5270:22-5270:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5294:21-5294:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5300:24-5300:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1733:19-1733:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2922:22-2922:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:2928:18-2928:151)
[Warning][Deadcode][CWE-571] condition 'i2 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:555:10-555:17)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5328:23-5328:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:1782:19-1782:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5377:18-5377:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5393:18-5393:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:3014:18-3014:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.ufo.BOUNDED-14.pals+Problem12_label07.c:5417:11-5417: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
