./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pals_lcr.3.ufo.BOUNDED-6.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.3.ufo.BOUNDED-6.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.3.ufo.BOUNDED-6.pals+Problem12_label07.c:264:3-279:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:5-5123: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] cannot unassume entry of type violation_sequence

[Info] runtime: 00:00:10.797
[Info] vars: 78393, evals: 71577

[Info] |called|=22

Memory statistics: total=22468.01MB, max=200.75MB, minor=22452.88MB, major=270.81MB, promoted=255.68MB
    minor collections=10714  major collections=15 compactions=0

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

[Info] runtime: 00:00:20.854
[Info] vars: 115581, evals: 108759

[Info] |called|=0

Memory statistics: total=43621.45MB, max=305.32MB, minor=43603.19MB, major=435.49MB, promoted=417.23MB
    minor collections=20800  major collections=17 compactions=0

[Warning][Deadcode] Function 'main2' has dead code:
  on line 5124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:5124-5124)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4108
  dead: 1
  total lines: 4109
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4016:20-4016:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1643:18-1643:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1658:19-1658:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2849:18-2849:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1692:18-1692:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2911:19-2911:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4146:21-4146:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:574:19-574:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1769:21-1769:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3055:19-3055:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1860:18-1860:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3062:21-3062:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:687:21-687:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4264:20-4264:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3076:18-3076:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1895:22-1895:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1902:22-1902:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3109:19-3109:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3129:18-3129:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2009:18-2009:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3188:21-3188:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3243:21-3243:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4451:21-4451:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:901:18-901:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:907:18-907:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2089:23-2089:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:914:18-914:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4487:22-4487:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2137:18-2137:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3315:18-3315:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3322:18-3322:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4568:21-4568:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4582:18-4582:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1032:18-1032:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1050:18-1050:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1056:19-1056:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1083:18-1083:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4653:21-4653:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4668:21-4668:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2288:18-2288:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2296:21-2296:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4685:20-4685:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4702:21-4702:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2316:21-2316:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3531:22-3531:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1178:18-1178:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2360:18-2360:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3553:19-3553:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2407:18-2407:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3602:22-3602:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1237:18-1237:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3622:19-3622:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4818:22-4818:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1251:18-1251:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1257:18-1257:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3663:21-3663:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3686:21-3686:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4886:18-4886:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1354:24-1354:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2548:18-2548:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2555:18-2555:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2561:21-2561:155)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4967:22-4967: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.ufo.BOUNDED-6.pals+Problem12_label07.c:78:5-78:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4991:21-4991:154)
[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.ufo.BOUNDED-6.pals+Problem12_label07.c:103:5-103:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:4997:24-4997: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.ufo.BOUNDED-6.pals+Problem12_label07.c:128:5-128:64)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1430:19-1430:172)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2619:22-2619:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2625:18-2625:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:5025:23-5025:154)
[Warning][Deadcode][CWE-571] condition 'i2 < 6' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:264:10-264:16)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1479:19-1479:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:5074:18-5074:154)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:5090:18-5090:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2711:18-2711: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:3935:18-3935:133)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1548:18-1548: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.ufo.BOUNDED-6.pals+Problem12_label07.c:5114:11-5114:12)
[Warning][Deadcode][CWE-571] condition 'a7 == 13' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1586:21-1586:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:2793:19-2793:151)
[Warning][Deadcode][CWE-571] condition 'a7 == 14' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pals_lcr.3.ufo.BOUNDED-6.pals+Problem12_label07.c:1603:21-1603:172)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
