./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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:479:3-502:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:5-5346: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.923
[Info] vars: 64080, evals: 57165

[Info] |called|=21

Memory statistics: total=20840.40MB, max=200.75MB, minor=20829.56MB, major=254.45MB, promoted=243.61MB
    minor collections=9939  major collections=15 compactions=0


[Info] runtime: 00:00:20.975
[Info] vars: 103769, evals: 96839

[Info] |called|=29

Memory statistics: total=41424.17MB, max=265.50MB, minor=41408.78MB, major=404.82MB, promoted=389.43MB
    minor collections=19753  major collections=17 compactions=0

[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:91:5-91:40)

[Info] runtime: 00:00:31.026
[Info] vars: 115860, evals: 108931

[Info] |called|=0

Memory statistics: total=61547.64MB, max=305.32MB, minor=61528.69MB, major=562.05MB, promoted=543.11MB
    minor collections=29349  major collections=19 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:504-504)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5347-5347)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4227
  dead: 2
  total lines: 4229
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1809:21-1809:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3016:19-3016:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1826:21-1826:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4239:20-4239:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1866:18-1866:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1881:19-1881:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3072:18-3072:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1915:18-1915:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3134:19-3134:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4369:21-4369:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:797:19-797:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1992:21-1992:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3278:19-3278:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2083:18-2083:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3285:21-3285:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:910:21-910:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4487:20-4487:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3299:18-3299:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2118:22-2118:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2125:22-2125:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3332:19-3332:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3352:18-3352:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2232:18-2232:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3411:21-3411:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3466:21-3466:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4674:21-4674:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1124:18-1124:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1130:18-1130:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2312:23-2312:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1137:18-1137:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4710:22-4710:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2360:18-2360:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3538:18-3538:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3545:18-3545:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4791:21-4791:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4805:18-4805:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1255:18-1255:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1273:18-1273:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1279:19-1279:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1306:18-1306:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4876:21-4876:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4891:21-4891:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2511:18-2511:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2519:21-2519:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4908:20-4908:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4925:21-4925:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2539:21-2539:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3754:22-3754:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1401:18-1401:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2583:18-2583:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3776:19-3776:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2630:18-2630:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3825:22-3825:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1460:18-1460:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3845:19-3845:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5041:22-5041:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1480:18-1480:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3886:21-3886:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:3909:21-3909:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5109:18-5109: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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:104:5-104:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1577:24-1577:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2771:18-2771: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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:129:5-129:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2778:18-2778:155)
[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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:154:5-154:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2784:21-2784:155)
[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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:179:5-179: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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:204:5-204:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5190:22-5190:154)
[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.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:229:5-229:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5214:21-5214:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5220:24-5220:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1653:19-1653:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2842:22-2842:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2848:18-2848:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5248:23-5248:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:479:10-479:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:479:10-479:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1702:19-1702:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5297:18-5297:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5313:18-5313:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:2934:18-2934:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:5337:11-5337:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:4158:18-4158:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.6_overflow.ufo.UNBOUNDED.pals+Problem12_label02.c:1771:18-1771:154)
[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)
