./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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:269:3-283:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:5-5127: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.905
[Info] vars: 73891, evals: 67038

[Info] |called|=30

Memory statistics: total=20685.64MB, max=200.75MB, minor=20670.55MB, major=256.98MB, promoted=241.88MB
    minor collections=9864  major collections=15 compactions=0

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

[Info] runtime: 00:00:20.991
[Info] vars: 115585, evals: 108724

[Info] |called|=0

Memory statistics: total=40952.53MB, max=265.50MB, minor=40934.65MB, major=408.62MB, promoted=390.74MB
    minor collections=19528  major collections=17 compactions=0


[Info] runtime: 00:00:31.058
[Info] vars: 115585, evals: 108724

[Info] |called|=0

Memory statistics: total=59708.25MB, max=351.13MB, minor=59686.74MB, major=572.00MB, promoted=550.49MB
    minor collections=28472  major collections=18 compactions=0

[Warning][Deadcode] Function 'main1' has dead code:
  on line 285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:285-285)
[Warning][Deadcode] Function 'main2' has dead code:
  on line 5128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5128-5128)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4110
  dead: 2
  total lines: 4112
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2797:19-2797:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1607:21-1607:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4020:20-4020:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1647:18-1647:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1662:19-1662:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2853:18-2853:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1696:18-1696:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2915:19-2915:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4150:21-4150:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:578:19-578:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1773:21-1773:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3059:19-3059:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1864:18-1864:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3066:21-3066:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:691:21-691:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4268:20-4268:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3080:18-3080:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1899:22-1899:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1906:22-1906:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3113:19-3113:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3133:18-3133:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2013:18-2013:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3192:21-3192:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3247:21-3247:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4455:21-4455:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:905:18-905:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:911:18-911:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2093:23-2093:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:918:18-918:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4491:22-4491:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2141:18-2141:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3319:18-3319:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3326:18-3326:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4572:21-4572:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4586:18-4586:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1036:18-1036:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1054:18-1054:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1060:19-1060:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1087:18-1087:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4657:21-4657:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4672:21-4672:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2292:18-2292:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2300:21-2300:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4689:20-4689:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4706:21-4706:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2320:21-2320:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3535:22-3535:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1182:18-1182:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2364:18-2364:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3557:19-3557:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2411:18-2411:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3606:22-3606:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1241:18-1241:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3626:19-3626:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4822:22-4822:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1255:18-1255:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1261:18-1261:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3667:21-3667:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3690:21-3690:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4890:18-4890:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1358:24-1358:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2552:18-2552:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2559:18-2559:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2565:21-2565:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4971:22-4971:154)
[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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:83:5-83: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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:108:5-108:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:4995:21-4995:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5001:24-5001: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.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:133:5-133:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1434:19-1434:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2623:22-2623:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2629:18-2629:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5029:23-5029:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:269:10-269:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:269:10-269:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:269:10-269:11)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1483:19-1483:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5078:18-5078:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5094:18-5094:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:2715:18-2715:151)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:3939:18-3939:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1552:18-1552:154)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:5118:11-5118:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3_overflow.ufo.UNBOUNDED.pals+Problem12_label05.c:1590:21-1590:151)
[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)
