./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.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.1.ufo.UNBOUNDED.pals+Problem12_label05.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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:338:3-355:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:5-5199: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] couldn't parse entry: find uuid

[Info] runtime: 00:00:11.017
[Info] vars: 67429, evals: 60556

[Info] |called|=25

Memory statistics: total=20281.43MB, max=200.75MB, minor=20267.39MB, major=252.21MB, promoted=238.17MB
    minor collections=9671  major collections=15 compactions=0


[Info] runtime: 00:00:21.076
[Info] vars: 110511, evals: 103627

[Info] |called|=26

Memory statistics: total=40196.07MB, max=265.50MB, minor=40180.62MB, major=394.92MB, promoted=379.47MB
    minor collections=19168  major collections=17 compactions=0


[Info] runtime: 00:00:31.157
[Info] vars: 115672, evals: 108789

[Info] |called|=0

Memory statistics: total=59332.55MB, max=351.13MB, minor=59313.50MB, major=551.43MB, promoted=532.38MB
    minor collections=28292  major collections=18 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:357-357)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5200-5200)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4150
  dead: 2
  total lines: 4152
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2869:19-2869:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1679:21-1679:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4092:20-4092:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1719:18-1719:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1734:19-1734:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2925:18-2925:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1768:18-1768:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2987:19-2987:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4222:21-4222:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:650:19-650:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1845:21-1845:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3131:19-3131:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1936:18-1936:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3138:21-3138:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:763:21-763:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4340:20-4340:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3152:18-3152:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1971:22-1971:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1978:22-1978:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3185:19-3185:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3205:18-3205:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2085:18-2085:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3264:21-3264:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3319:21-3319:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4527:21-4527:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:977:18-977:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:983:18-983:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2165:23-2165:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:990:18-990:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4563:22-4563:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2213:18-2213:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3391:18-3391:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3398:18-3398:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4644:21-4644:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4658:18-4658:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1108:18-1108:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1126:18-1126:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1132:19-1132:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1159:18-1159:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4729:21-4729:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4744:21-4744:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2364:18-2364:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2372:21-2372:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4761:20-4761:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4778:21-4778:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2392:21-2392:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3607:22-3607:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1254:18-1254:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2436:18-2436:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3629:19-3629:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2483:18-2483:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3678:22-3678:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1313:18-1313:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3698:19-3698:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4894:22-4894:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1327:18-1327:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1333:18-1333:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3739:21-3739:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:3762:21-3762:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4962:18-4962:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1430:24-1430:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2624:18-2624:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2631:18-2631:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2637:21-2637:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5043:22-5043: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:93:5-93: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:118:5-118: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:143:5-143:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5067:21-5067: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:168:5-168:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5073:24-5073:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1506:19-1506:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2695:22-2695:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2701:18-2701:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5101:23-5101: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:338:10-338: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:338:10-338:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1555:19-1555:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5150:18-5150:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5166:18-5166:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:2787:18-2787: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:4011:18-4011:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1624:18-1624: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.1.ufo.UNBOUNDED.pals+Problem12_label05.c:5190:11-5190:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.4.1.ufo.UNBOUNDED.pals+Problem12_label05.c:1662:21-1662:151)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
