./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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:557:3-584:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:5-5428: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.850
[Info] vars: 63255, evals: 56387

[Info] |called|=29

Memory statistics: total=21406.56MB, max=174.57MB, minor=21395.75MB, major=262.59MB, promoted=251.79MB
    minor collections=10210  major collections=15 compactions=0


[Info] runtime: 00:00:20.933
[Info] vars: 100666, evals: 93784

[Info] |called|=25

Memory statistics: total=42120.39MB, max=265.50MB, minor=42105.05MB, major=413.45MB, promoted=398.11MB
    minor collections=20086  major collections=17 compactions=0

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

[Info] runtime: 00:00:31.000
[Info] vars: 115978, evals: 109096

[Info] |called|=0

Memory statistics: total=63232.14MB, max=351.13MB, minor=63213.46MB, major=572.64MB, promoted=553.96MB
    minor collections=30153  major collections=19 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5429-5429)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4272
  dead: 1
  total lines: 4273
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4240:18-4240:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1853:18-1853:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1891:21-1891:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3098:19-3098:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1908:21-1908:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4321:20-4321:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1948:18-1948:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1963:19-1963:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3154:18-3154:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1997:18-1997:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3216:19-3216:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4451:21-4451:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:879:19-879:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2074:21-2074:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3360:19-3360:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2165:18-2165:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3367:21-3367:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:992:21-992:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4569:20-4569:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3381:18-3381:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2200:22-2200:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2207:22-2207:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3414:19-3414:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3434:18-3434:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2314:18-2314:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3493:21-3493:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3548:21-3548:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4756:21-4756:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1206:18-1206:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1212:18-1212:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2394:23-2394:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1219:18-1219:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4792:22-4792:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2442:18-2442:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3620:18-3620:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3627:18-3627:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4873:21-4873:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4887:18-4887:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1337:18-1337:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1355:18-1355:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1361:19-1361:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1388:18-1388:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4958:21-4958:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4973:21-4973:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2593:18-2593:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2601:21-2601:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:4990:20-4990:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5007:21-5007:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2621:21-2621:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3836:22-3836:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1483:18-1483:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2665:18-2665:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3858:19-3858:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2712:18-2712:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3907:22-3907:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1542:18-1542:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3927:19-3927:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5123:22-5123:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1556:18-1556:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1562:18-1562:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3968:21-3968:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3991:21-3991:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5191:18-5191: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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:111:5-111: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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:136:5-136: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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:161:5-161:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1659:24-1659:172)
[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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:186:5-186:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2853:18-2853:155)
[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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:211:5-211:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2860:18-2860:155)
[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.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:236:5-236:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2866:21-2866:155)
[Warning][Deadcode][CWE-571] condition '(int )p7_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:261:5-261:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5272:22-5272:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5296:21-5296:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5302:24-5302:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1735:19-1735:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2924:22-2924:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:2930:18-2930:151)
[Warning][Deadcode][CWE-571] condition 'i2 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:557:10-557:17)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5330:23-5330:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:1784:19-1784:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5379:18-5379:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5395:18-5395:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:3016:18-3016:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.BOUNDED-14.pals+Problem12_label01.c:5419:11-5419:12)

[Info] runtime: 00:00:41.079
[Info] vars: 115978, evals: 109096

[Info] |called|=0

Memory statistics: total=81148.22MB, max=403.80MB, minor=81126.09MB, major=712.81MB, promoted=690.68MB
    minor collections=38696  major collections=20 compactions=0

[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)
