./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.3.ufo.UNBOUNDED.pals+Problem12_label00.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.3.ufo.UNBOUNDED.pals+Problem12_label00.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.3.ufo.UNBOUNDED.pals+Problem12_label00.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.3.ufo.UNBOUNDED.pals+Problem12_label00.c:270:3-284:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:5-5128: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.853
[Info] vars: 77905, evals: 71049

[Info] |called|=23

Memory statistics: total=21980.53MB, max=200.75MB, minor=21965.40MB, major=266.82MB, promoted=251.69MB
    minor collections=10481  major collections=15 compactions=0


[Info] runtime: 00:00:20.920
[Info] vars: 115590, evals: 108728

[Info] |called|=0

Memory statistics: total=42071.33MB, max=265.50MB, minor=42053.40MB, major=421.05MB, promoted=403.13MB
    minor collections=20061  major collections=17 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:286-286)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5129-5129)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4112
  dead: 2
  total lines: 4114
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2798:19-2798:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1608:21-1608:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4021:20-4021:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1648:18-1648:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1663:19-1663:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2854:18-2854:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1697:18-1697:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2916:19-2916:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4151:21-4151:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:579:19-579:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1774:21-1774:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3060:19-3060:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1865:18-1865:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3067:21-3067:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:692:21-692:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4269:20-4269:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3081:18-3081:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1900:22-1900:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1907:22-1907:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3114:19-3114:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3134:18-3134:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2014:18-2014:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3193:21-3193:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3248:21-3248:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4456:21-4456:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:906:18-906:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:912:18-912:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2094:23-2094:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:919:18-919:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4492:22-4492:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2142:18-2142:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3320:18-3320:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3327:18-3327:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4573:21-4573:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4587:18-4587:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1037:18-1037:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1055:18-1055:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1061:19-1061:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1088:18-1088:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4658:21-4658:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4673:21-4673:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2293:18-2293:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2301:21-2301:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4690:20-4690:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4707:21-4707:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2321:21-2321:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3536:22-3536:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1183:18-1183:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2365:18-2365:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3558:19-3558:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2412:18-2412:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3607:22-3607:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1242:18-1242:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3627:19-3627:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4823:22-4823:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1256:18-1256:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1262:18-1262:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3668:21-3668:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3691:21-3691:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4891:18-4891:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1359:24-1359:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2553:18-2553:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2560:18-2560:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2566:21-2566:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4972:22-4972: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.3.ufo.UNBOUNDED.pals+Problem12_label00.c:84:5-84: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.3.ufo.UNBOUNDED.pals+Problem12_label00.c:109:5-109:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:4996:21-4996:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5002:24-5002: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.3.ufo.UNBOUNDED.pals+Problem12_label00.c:134:5-134:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1435:19-1435:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2624:22-2624:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2630:18-2630:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5030:23-5030:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:270:10-270:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:270:10-270:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:270:10-270:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1484:19-1484:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5079:18-5079:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5095:18-5095:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:2716:18-2716:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:3940:18-3940:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1553:18-1553:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:5119:11-5119:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c:1591:21-1591: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)
