./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.BOUNDED-8.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.BOUNDED-8.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.BOUNDED-8.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, main__i2, node1__m1___0, node1__m1___1, node2__m2___0, node3__m3___0, node4__m4___0, node2__m2___1, node3__m3___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][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:370:2-370:28)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:159-159)
  on line 177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:177-177)
  on line 195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:195-195)
  on line 213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:213-213)
  on line 240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:240-240)
  on line 258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:258-258)
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:357-357)
  on line 471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:471-471)
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:516-516)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:561-561)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:607-607)
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:680-680)
  on line 704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:704-704)
  on line 728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:728-728)
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:753-753)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:759-759)
  on line 766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:766-766)
  on line 771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:771-771)
  on line 777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:777-777)
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:783-783)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:788-788)
  on line 796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:796-796)
  on line 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:801-801)
  on line 809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:809-809)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:814-814)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:822-822)
  on line 827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:827-827)
  on line 835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:835-835)
  on line 840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:840-840)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 275
  dead: 31 (2 in uncalled functions)
  total lines: 306
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:594:6-594: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.BOUNDED-8.pals.c.v+nlh-reducer.c:596:6-596:21)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:175:6-175: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.BOUNDED-8.pals.c.v+nlh-reducer.c:182:6-182: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.BOUNDED-8.pals.c.v+nlh-reducer.c:184:6-184: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.BOUNDED-8.pals.c.v+nlh-reducer.c:193:6-193: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.BOUNDED-8.pals.c.v+nlh-reducer.c:200:6-200: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.BOUNDED-8.pals.c.v+nlh-reducer.c:202:6-202: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.BOUNDED-8.pals.c.v+nlh-reducer.c:211:6-211: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.BOUNDED-8.pals.c.v+nlh-reducer.c:218:6-218: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.BOUNDED-8.pals.c.v+nlh-reducer.c:220:6-220: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.BOUNDED-8.pals.c.v+nlh-reducer.c:236:10-236: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.BOUNDED-8.pals.c.v+nlh-reducer.c:238:7-238: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.BOUNDED-8.pals.c.v+nlh-reducer.c:244:10-244: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.BOUNDED-8.pals.c.v+nlh-reducer.c:246:7-246: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.BOUNDED-8.pals.c.v+nlh-reducer.c:256:6-256:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:264:6-264:18)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:269:6-269:19)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:274:7-274:38)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:284:6-284: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.BOUNDED-8.pals.c.v+nlh-reducer.c:458:6-458: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.BOUNDED-8.pals.c.v+nlh-reducer.c:460:6-460:21)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:288:7-288: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.BOUNDED-8.pals.c.v+nlh-reducer.c:298:6-298: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.BOUNDED-8.pals.c.v+nlh-reducer.c:302:7-302: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.BOUNDED-8.pals.c.v+nlh-reducer.c:503:6-503: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.BOUNDED-8.pals.c.v+nlh-reducer.c:505:6-505: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.BOUNDED-8.pals.c.v+nlh-reducer.c:312:6-312: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.BOUNDED-8.pals.c.v+nlh-reducer.c:316:7-316:38)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:141:6-141: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.BOUNDED-8.pals.c.v+nlh-reducer.c:548:6-548: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.BOUNDED-8.pals.c.v+nlh-reducer.c:550:6-550:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 8' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.4.1.ufo.BOUNDED-8.pals.c.v+nlh-reducer.c:152:6-152:18)
[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.BOUNDED-8.pals.c.v+nlh-reducer.c:157:6-157: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.BOUNDED-8.pals.c.v+nlh-reducer.c:164:6-164: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.BOUNDED-8.pals.c.v+nlh-reducer.c:166:6-166: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
