./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.8.ufo.BOUNDED-16.pals+Problem12_label07.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.8.ufo.BOUNDED-16.pals+Problem12_label07.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.8.ufo.BOUNDED-16.pals+Problem12_label07.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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:5-5514: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.899
[Info] vars: 57115, evals: 50233

[Info] |called|=33

Memory statistics: total=18234.36MB, max=174.57MB, minor=18223.66MB, major=239.07MB, promoted=228.37MB
    minor collections=8697  major collections=15 compactions=0


[Info] runtime: 00:00:20.984
[Info] vars: 85362, evals: 78468

[Info] |called|=21

Memory statistics: total=35318.12MB, max=230.87MB, minor=35302.91MB, major=367.97MB, promoted=352.76MB
    minor collections=16842  major collections=17 compactions=0


[Info] runtime: 00:00:31.052
[Info] vars: 108642, evals: 101744

[Info] |called|=26

Memory statistics: total=52223.12MB, max=305.32MB, minor=52207.69MB, major=480.43MB, promoted=465.00MB
    minor collections=24904  major collections=18 compactions=0

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

[Info] runtime: 00:00:41.135
[Info] vars: 116052, evals: 109154

[Info] |called|=0

Memory statistics: total=67948.19MB, max=351.13MB, minor=67929.29MB, major=607.40MB, promoted=588.50MB
    minor collections=32401  major collections=19 compactions=0


[Info] runtime: 00:00:51.226
[Info] vars: 116052, evals: 109154

[Info] |called|=0

Memory statistics: total=85187.54MB, max=403.80MB, minor=85167.36MB, major=724.06MB, promoted=703.88MB
    minor collections=40621  major collections=20 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5515-5515)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4316
  dead: 1
  total lines: 4317
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4326:18-4326:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1939:18-1939:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1977:21-1977:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3184:19-3184:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1994:21-1994:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4407:20-4407:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2034:18-2034:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2049:19-2049:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3240:18-3240:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2083:18-2083:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3302:19-3302:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4537:21-4537:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:965:19-965:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2160:21-2160:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3446:19-3446:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2251:18-2251:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3453:21-3453:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1078:21-1078:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4655:20-4655:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3467:18-3467:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2286:22-2286:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2293:22-2293:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3500:19-3500:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3520:18-3520:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2400:18-2400:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3579:21-3579:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3634:21-3634:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4842:21-4842:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1292:18-1292:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1298:18-1298:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2480:23-2480:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1305:18-1305:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4878:22-4878:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2528:18-2528:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3706:18-3706:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3713:18-3713:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4959:21-4959:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4973:18-4973:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1423:18-1423:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1441:18-1441:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1447:19-1447:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1474:18-1474:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5044:21-5044:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5059:21-5059:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2679:18-2679:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2687:21-2687:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5076:20-5076:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5093:21-5093:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2707:21-2707:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3922:22-3922:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1569:18-1569:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2751:18-2751:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3944:19-3944:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2798:18-2798:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3993:22-3993:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1628:18-1628:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4013:19-4013:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5209:22-5209:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1642:18-1642:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1648:18-1648:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4054:21-4054:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:4077:21-4077:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5277:18-5277: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:116:5-116: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:141:5-141: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:166:5-166: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:191:5-191: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:216:5-216:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1745:24-1745:172)
[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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:241:5-241:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2939:18-2939:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2946:18-2946: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.8.ufo.BOUNDED-16.pals+Problem12_label07.c:266:5-266:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:2952:21-2952:155)
[Warning][Deadcode][CWE-571] condition '(int )p8_new == (int )nomsg' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:291:5-291:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5358:22-5358:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5382:21-5382:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5388:24-5388:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1821:19-1821:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3010:22-3010:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3016:18-3016:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5416:23-5416:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:1870:19-1870:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5465:18-5465:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5481:18-5481:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:3102:18-3102:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.8.ufo.BOUNDED-16.pals+Problem12_label07.c:5505:11-5505: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)
