./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.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.7.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.7.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.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:560:3-586:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5421:5-5430: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.766
[Info] vars: 62765, evals: 55825

[Info] |called|=28

Memory statistics: total=20834.41MB, max=200.75MB, minor=20823.61MB, major=258.25MB, promoted=247.45MB
    minor collections=9937  major collections=15 compactions=0


[Info] runtime: 00:00:20.842
[Info] vars: 97409, evals: 90455

[Info] |called|=24

Memory statistics: total=40247.01MB, max=265.50MB, minor=40231.69MB, major=400.04MB, promoted=384.73MB
    minor collections=19192  major collections=17 compactions=0


[Info] runtime: 00:00:30.905
[Info] vars: 115969, evals: 109014

[Info] |called|=0

Memory statistics: total=59203.84MB, max=305.32MB, minor=59185.53MB, major=540.39MB, promoted=522.08MB
    minor collections=28231  major collections=19 compactions=0


[Info] runtime: 00:00:40.972
[Info] vars: 115969, evals: 109014

[Info] |called|=0

Memory statistics: total=78819.43MB, max=351.13MB, minor=78799.25MB, major=679.30MB, promoted=659.11MB
    minor collections=37585  major collections=20 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:588-588)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5431-5431)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4273
  dead: 2
  total lines: 4275
[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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4242:18-4242:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1855:18-1855: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1893:21-1893:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3100:19-3100:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1910:21-1910:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4323:20-4323:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1950:18-1950:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1965:19-1965:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3156:18-3156:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1999:18-1999:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3218:19-3218:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4453:21-4453:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:881:19-881:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2076:21-2076:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3362:19-3362:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2167:18-2167:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3369:21-3369:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:994:21-994:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4571:20-4571:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3383:18-3383:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2202:22-2202:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2209:22-2209:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3416:19-3416:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3436:18-3436:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2316:18-2316:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3495:21-3495:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3550:21-3550:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4758:21-4758:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1208:18-1208:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1214:18-1214:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2396:23-2396:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1221:18-1221:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4794:22-4794:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2444:18-2444:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3622:18-3622:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3629:18-3629:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4875:21-4875:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4889:18-4889:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1339:18-1339:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1357:18-1357:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1363:19-1363:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1390:18-1390:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4960:21-4960:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4975:21-4975:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2595:18-2595:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2603:21-2603:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:4992:20-4992:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5009:21-5009:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2623:21-2623:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3838:22-3838:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1485:18-1485:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2667:18-2667:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3860:19-3860:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2714:18-2714:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3909:22-3909:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1544:18-1544:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3929:19-3929:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5125:22-5125:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1558:18-1558:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1564:18-1564:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3970:21-3970:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3993:21-3993:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5193:18-5193: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.UNBOUNDED.pals+Problem12_label04.c:114:5-114: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.UNBOUNDED.pals+Problem12_label04.c:139:5-139: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.UNBOUNDED.pals+Problem12_label04.c:164:5-164:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1661:24-1661: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.UNBOUNDED.pals+Problem12_label04.c:189:5-189:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2855:18-2855: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.UNBOUNDED.pals+Problem12_label04.c:214:5-214:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2862:18-2862: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.UNBOUNDED.pals+Problem12_label04.c:239:5-239:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2868:21-2868: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.UNBOUNDED.pals+Problem12_label04.c:264:5-264:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5274:22-5274:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5298:21-5298:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5304:24-5304:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1737:19-1737:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2926:22-2926:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:2932:18-2932: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.UNBOUNDED.pals+Problem12_label04.c:560:10-560:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5332:23-5332: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.UNBOUNDED.pals+Problem12_label04.c:560:10-560:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:1786:19-1786:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5381:18-5381:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:5397:18-5397:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.7.1.ufo.UNBOUNDED.pals+Problem12_label04.c:3018:18-3018: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421: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.UNBOUNDED.pals+Problem12_label04.c:5421:11-5421: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)
