./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.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.1.ufo.UNBOUNDED.pals+Problem12_label02.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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:408:3-428:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:5-5272: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.915
[Info] vars: 66460, evals: 59564

[Info] |called|=78

Memory statistics: total=21332.57MB, max=200.75MB, minor=21318.57MB, major=261.31MB, promoted=247.31MB
    minor collections=10172  major collections=15 compactions=0


[Info] runtime: 00:00:20.993
[Info] vars: 107179, evals: 100273

[Info] |called|=21

Memory statistics: total=41446.36MB, max=265.50MB, minor=41430.94MB, major=403.22MB, promoted=387.80MB
    minor collections=19764  major collections=17 compactions=0


[Info] runtime: 00:00:31.038
[Info] vars: 115768, evals: 108862

[Info] |called|=0

Memory statistics: total=61954.69MB, max=305.32MB, minor=61935.69MB, major=567.35MB, promoted=548.35MB
    minor collections=29542  major collections=19 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:430-430)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5273-5273)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4189
  dead: 2
  total lines: 4191
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1735:21-1735:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2942:19-2942:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1752:21-1752:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4165:20-4165:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1792:18-1792:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1807:19-1807:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2998:18-2998:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1841:18-1841:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3060:19-3060:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4295:21-4295:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:723:19-723:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1918:21-1918:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3204:19-3204:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2009:18-2009:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3211:21-3211:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:836:21-836:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4413:20-4413:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3225:18-3225:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2044:22-2044:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2051:22-2051:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3258:19-3258:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3278:18-3278:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2158:18-2158:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3337:21-3337:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3392:21-3392:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4600:21-4600:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1050:18-1050:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1056:18-1056:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2238:23-2238:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1063:18-1063:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4636:22-4636:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2286:18-2286:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3464:18-3464:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3471:18-3471:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4717:21-4717:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4731:18-4731:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1181:18-1181:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1199:18-1199:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1205:19-1205:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1232:18-1232:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4802:21-4802:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4817:21-4817:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2437:18-2437:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2445:21-2445:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4834:20-4834:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4851:21-4851:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2465:21-2465:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3680:22-3680:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1327:18-1327:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2509:18-2509:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3702:19-3702:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2556:18-2556:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3751:22-3751:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1386:18-1386:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3771:19-3771:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4967:22-4967:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1400:18-1400:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1406:18-1406:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3812:21-3812:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:3835:21-3835:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5035:18-5035:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1503:24-1503:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2697:18-2697:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2704:18-2704: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:100:5-100:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2710:21-2710: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:125:5-125:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5116:22-5116: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:150:5-150: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:175:5-175: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:200:5-200:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5140:21-5140:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5146:24-5146:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1579:19-1579:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2768:22-2768:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2774:18-2774:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5174:23-5174: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:408:10-408:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:408:10-408:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1628:19-1628:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5223:18-5223:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5239:18-5239:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:2860:18-2860: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:4084:18-4084:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.UNBOUNDED.pals+Problem12_label02.c:1697:18-1697: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.1.ufo.UNBOUNDED.pals+Problem12_label02.c:5263:11-5263: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
