./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.5.1.ufo.BOUNDED-10.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.5.1.ufo.BOUNDED-10.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.5.1.ufo.BOUNDED-10.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.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:405:3-426:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5261:5-5270: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.874
[Info] vars: 65565, evals: 58728

[Info] |called|=28

Memory statistics: total=20573.93MB, max=200.75MB, minor=20559.93MB, major=254.91MB, promoted=240.91MB
    minor collections=9811  major collections=15 compactions=0


[Info] runtime: 00:00:20.949
[Info] vars: 106762, evals: 99911

[Info] |called|=25

Memory statistics: total=41197.88MB, max=265.50MB, minor=41182.46MB, major=401.32MB, promoted=385.90MB
    minor collections=19646  major collections=17 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:82:5-82:31)

[Info] runtime: 00:00:31.000
[Info] vars: 115777, evals: 108926

[Info] |called|=0

Memory statistics: total=61389.61MB, max=305.32MB, minor=61370.61MB, major=562.57MB, promoted=543.57MB
    minor collections=29273  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5271-5271)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4188
  dead: 1
  total lines: 4189
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1733:21-1733:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2940:19-2940:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1750:21-1750:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4163:20-4163:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1790:18-1790:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1805:19-1805:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2996:18-2996:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1839:18-1839:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3058:19-3058:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4293:21-4293:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:721:19-721:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1916:21-1916:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3202:19-3202:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2007:18-2007:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3209:21-3209:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:834:21-834:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4411:20-4411:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3223:18-3223:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2042:22-2042:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2049:22-2049:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3256:19-3256:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3276:18-3276:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2156:18-2156:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3335:21-3335:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3390:21-3390:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4598:21-4598:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1048:18-1048:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1054:18-1054:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2236:23-2236:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1061:18-1061:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4634:22-4634:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2284:18-2284:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3462:18-3462:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3469:18-3469:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4715:21-4715:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4729:18-4729:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1179:18-1179:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1197:18-1197:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1203:19-1203:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1230:18-1230:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4800:21-4800:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4815:21-4815:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2435:18-2435:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2443:21-2443:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4832:20-4832:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4849:21-4849:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2463:21-2463:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3678:22-3678:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1325:18-1325:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2507:18-2507:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3700:19-3700:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2554:18-2554:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3749:22-3749:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1384:18-1384:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3769:19-3769:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4965:22-4965:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1398:18-1398:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1404:18-1404:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3810:21-3810:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:3833:21-3833:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5033:18-5033:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1501:24-1501:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2695:18-2695:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2702:18-2702: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.BOUNDED-10.pals+Problem12_label04.c:97:5-97:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2708:21-2708: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.BOUNDED-10.pals+Problem12_label04.c:122:5-122:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5114:22-5114: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.BOUNDED-10.pals+Problem12_label04.c:147:5-147: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.BOUNDED-10.pals+Problem12_label04.c:172:5-172: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.BOUNDED-10.pals+Problem12_label04.c:197:5-197:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5138:21-5138:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5144:24-5144:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1577:19-1577:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2766:22-2766:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2772:18-2772:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5172:23-5172:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:405:10-405:17)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1626:19-1626:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5221:18-5221:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:5237:18-5237:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:2858:18-2858: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:4082:18-4082:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.5.1.ufo.BOUNDED-10.pals+Problem12_label04.c:1695:18-1695: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.BOUNDED-10.pals+Problem12_label04.c:5261:11-5261:12)
[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)
