./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.UNBOUNDED.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.UNBOUNDED.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.UNBOUNDED.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.UNBOUNDED.pals+Problem12_label03.c:480:3-503:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5338:5-5347: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.854
[Info] vars: 65321, evals: 58405

[Info] |called|=24

Memory statistics: total=21623.07MB, max=200.75MB, minor=21612.22MB, major=261.26MB, promoted=250.42MB
    minor collections=10312  major collections=15 compactions=0


[Info] runtime: 00:00:20.942
[Info] vars: 102919, evals: 95988

[Info] |called|=25

Memory statistics: total=41286.97MB, max=265.50MB, minor=41271.60MB, major=404.31MB, promoted=388.94MB
    minor collections=19688  major collections=17 compactions=0


[Info] runtime: 00:00:31.008
[Info] vars: 115865, evals: 108935

[Info] |called|=0

Memory statistics: total=59812.61MB, max=305.32MB, minor=59793.70MB, major=548.84MB, promoted=529.93MB
    minor collections=28521  major collections=19 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:505-505)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5348-5348)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4229
  dead: 2
  total lines: 4231
[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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1810:21-1810:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3017:19-3017:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1827:21-1827:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4240:20-4240:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1867:18-1867:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1882:19-1882:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3073:18-3073:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1916:18-1916:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3135:19-3135:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4370:21-4370:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:798:19-798:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1993:21-1993:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3279:19-3279:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2084:18-2084:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3286:21-3286:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:911:21-911:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4488:20-4488:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3300:18-3300:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2119:22-2119:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2126:22-2126:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3333:19-3333:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3353:18-3353:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2233:18-2233:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3412:21-3412:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3467:21-3467:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4675:21-4675:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1125:18-1125:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1131:18-1131:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2313:23-2313:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1138:18-1138:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4711:22-4711:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2361:18-2361:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3539:18-3539:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3546:18-3546:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4792:21-4792:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4806:18-4806:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1256:18-1256:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1274:18-1274:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1280:19-1280:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1307:18-1307:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4877:21-4877:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4892:21-4892:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2512:18-2512:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2520:21-2520:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4909:20-4909:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4926:21-4926:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2540:21-2540:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3755:22-3755:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1402:18-1402:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2584:18-2584:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3777:19-3777:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2631:18-2631:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3826:22-3826:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1461:18-1461:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3846:19-3846:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5042:22-5042:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1475:18-1475:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1481:18-1481:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3887:21-3887:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:3910:21-3910:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5110:18-5110: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.UNBOUNDED.pals+Problem12_label03.c:105:5-105:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1578:24-1578:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2772:18-2772: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.UNBOUNDED.pals+Problem12_label03.c:130:5-130:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2779:18-2779: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.UNBOUNDED.pals+Problem12_label03.c:155:5-155:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2785:21-2785: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.UNBOUNDED.pals+Problem12_label03.c:180:5-180: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.UNBOUNDED.pals+Problem12_label03.c:205:5-205:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5191:22-5191: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.UNBOUNDED.pals+Problem12_label03.c:230:5-230:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5215:21-5215:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5221:24-5221:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1654:19-1654:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2843:22-2843:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2849:18-2849:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5249:23-5249:154)
[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.UNBOUNDED.pals+Problem12_label03.c:480:10-480:11)
[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.UNBOUNDED.pals+Problem12_label03.c:480:10-480:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1703:19-1703:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5298:18-5298:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:5314:18-5314:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:2935:18-2935: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338: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.UNBOUNDED.pals+Problem12_label03.c:5338:11-5338:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:4159:18-4159:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.ufo.UNBOUNDED.pals+Problem12_label03.c:1772:18-1772: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
