./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.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/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.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 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] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] nomsg, id1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, node1__m1___0, node1__m1___1, node2__m2___0, node3__m3___0, node4__m4___0, node2__m2___1, node3__m3___1, node4__m4___1, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:156-156)
  on line 174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:174-174)
  on line 192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:192-192)
  on line 210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:210-210)
  on line 237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:237-237)
  on line 255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:255-255)
  on line 266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:266-266)
  on line 354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:354-354)
  on line 467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:467-467)
  on line 512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:512-512)
  on line 557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:557-557)
  on line 608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:608-608)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:675-675)
  on line 699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:699-699)
  on line 723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:723-723)
  on line 749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:749-749)
  on line 757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:757-757)
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:762-762)
  on line 768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:768-768)
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:774-774)
  on line 779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:779-779)
  on line 787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:787-787)
  on line 792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:792-792)
  on line 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:800-800)
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:805-805)
  on line 813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:813-813)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:818-818)
  on line 826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:826-826)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 267
  dead: 30 (2 in uncalled functions)
  total lines: 297
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:172:6-172:19)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:179:6-179:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:181:6-181:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:190:6-190:19)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:197:6-197:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:199:6-199:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:208:6-208:19)
[Warning][Deadcode][CWE-571] condition '(int )send4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:215:6-215:20)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:217:6-217:21)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:233:10-233:66)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:235:7-235:20)
[Warning][Deadcode][CWE-571] condition '(((int )st1 + (int )st2) + (int )st3) + (int )st4 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:241:10-241:66)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 4' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:243:7-243:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:253:6-253:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:262:6-262:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:264:6-264:15)
[Warning][Deadcode][CWE-571] condition '(int )node1__m1___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:273:7-273:38)
[Warning][Deadcode][CWE-571] condition '(int )send4 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:454:6-454:20)
[Warning][Deadcode][CWE-571] condition '(int )p4_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:456:6-456:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:283:6-283:19)
[Warning][Deadcode][CWE-571] condition '(int )node2__m2___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:287:7-287:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:297:6-297:19)
[Warning][Deadcode][CWE-571] condition '(int )node3__m3___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:301:7-301:38)
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:499:6-499:20)
[Warning][Deadcode][CWE-571] condition '(int )p3_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:501:6-501:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:311:6-311:19)
[Warning][Deadcode][CWE-571] condition '(int )node4__m4___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:315:7-315:38)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:544:6-544:20)
[Warning][Deadcode][CWE-571] condition '(int )p2_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:546:6-546:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:140:6-140:19)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:154:6-154:19)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:161:6-161:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:163:6-163:21)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:595:6-595:20)
[Warning][Deadcode][CWE-571] condition '(int )p1_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:597:6-597:21)
[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
