./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.6.1.ufo.UNBOUNDED.pals+Problem12_label04.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.6.1.ufo.UNBOUNDED.pals+Problem12_label04.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.1.ufo.UNBOUNDED.pals+Problem12_label04.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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:482:3-505:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:5-5349: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:10.828
[Info] vars: 65786, evals: 58870

[Info] |called|=30

Memory statistics: total=21871.59MB, max=200.75MB, minor=21857.58MB, major=265.85MB, promoted=251.84MB
    minor collections=10430  major collections=15 compactions=0


[Info] runtime: 00:00:20.886
[Info] vars: 105772, evals: 98840

[Info] |called|=20

Memory statistics: total=42826.34MB, max=265.50MB, minor=42810.94MB, major=414.02MB, promoted=398.62MB
    minor collections=20422  major collections=17 compactions=0


[Info] runtime: 00:00:30.925
[Info] vars: 115867, evals: 108937

[Info] |called|=0

Memory statistics: total=63429.66MB, max=351.13MB, minor=63410.67MB, major=574.99MB, promoted=556.00MB
    minor collections=30246  major collections=19 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:507-507)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5350-5350)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4230
  dead: 2
  total lines: 4232
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1812:21-1812:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3019:19-3019:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1829:21-1829:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4242:20-4242:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1869:18-1869:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1884:19-1884:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3075:18-3075:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1918:18-1918:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3137:19-3137:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4372:21-4372:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:800:19-800:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1995:21-1995:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3281:19-3281:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2086:18-2086:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3288:21-3288:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:913:21-913:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4490:20-4490:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3302:18-3302:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2121:22-2121:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2128:22-2128:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3335:19-3335:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3355:18-3355:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2235:18-2235:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3414:21-3414:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3469:21-3469:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4677:21-4677:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1127:18-1127:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1133:18-1133:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2315:23-2315:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1140:18-1140:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4713:22-4713:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2363:18-2363:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3541:18-3541:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3548:18-3548:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4794:21-4794:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4808:18-4808:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1258:18-1258:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1276:18-1276:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1282:19-1282:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1309:18-1309:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4879:21-4879:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4894:21-4894:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2514:18-2514:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2522:21-2522:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4911:20-4911:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4928:21-4928:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2542:21-2542:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3757:22-3757:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1404:18-1404:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2586:18-2586:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3779:19-3779:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2633:18-2633:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3828:22-3828:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1463:18-1463:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3848:19-3848:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5044:22-5044:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1477:18-1477:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1483:18-1483:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3889:21-3889:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3912:21-3912:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5112:18-5112: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:107:5-107:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1580:24-1580:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2774:18-2774: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:132:5-132:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2781:18-2781: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:157:5-157:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2787:21-2787: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:182:5-182: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:207:5-207:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5193:22-5193: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:232:5-232:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5217:21-5217:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5223:24-5223:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1656:19-1656:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2845:22-2845:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2851:18-2851:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5251:23-5251: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:482:10-482: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:482:10-482:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1705:19-1705:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5300:18-5300:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5316:18-5316:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2937:18-2937: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340: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.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5340:11-5340:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4161:18-4161:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1774:18-1774:154)
[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)
