./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.5.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.5.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.5.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, __return_main, 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, node5__m5___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][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:19:1-21:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:186-186)
  on line 204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:204-204)
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:222-222)
  on line 240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:240-240)
  on line 258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:258-258)
  on line 287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:287-287)
  on line 305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:305-305)
  on line 316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:316-316)
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:420-420)
  on line 540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:540-540)
  on line 585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:585-585)
  on line 630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:630-630)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:675-675)
  on line 726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:726-726)
  on line 793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:793-793)
  on line 817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:817-817)
  on line 841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:841-841)
  on line 865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:865-865)
  on line 891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:891-891)
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:899-899)
  on line 904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:904-904)
  on line 910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:910-910)
  on line 916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:916-916)
  on line 921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:921-921)
  on line 929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:929-929)
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:934-934)
  on line 942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:942-942)
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:947-947)
  on line 955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:955-955)
  on line 960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:960-960)
  on line 968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:968-968)
  on line 973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:973-973)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:981-981)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 317
  dead: 35 (2 in uncalled functions)
  total lines: 352
[Warning][Deadcode][CWE-571] condition '(int )node5__m5___0 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:379:7-379:38)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:184:6-184: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:191:6-191: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:193:6-193:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:202:6-202: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:617:6-617: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:619:6-619:21)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:209:6-209: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:211:6-211:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:220:6-220: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:227:6-227: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:229:6-229:21)
[Warning][Deadcode][CWE-571] condition '(int )send2 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:662:6-662: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:664:6-664:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode4 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:238:6-238: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:245:6-245: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:247:6-247:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode5 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:256:6-256:19)
[Warning][Deadcode][CWE-571] condition '(int )send5 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:263:6-263:20)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:265:6-265: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:713:6-713: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:715:6-715:21)
[Warning][Deadcode][CWE-571] condition '((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:283:11-283:81)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:285:7-285:20)
[Warning][Deadcode][CWE-571] condition '((((int )st1 + (int )st2) + (int )st3) + (int )st4) + (int )st5 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:291:11-291:81)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:293:7-293: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:303:6-303:22)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:312:6-312:19)
[Warning][Deadcode][CWE-570] condition '(int )r1 == 255' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:314:6-314: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:323:7-323:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:333:6-333: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:337:7-337:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:347:6-347:19)
[Warning][Deadcode][CWE-571] condition '(int )send5 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:527:6-527:20)
[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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:351:7-351:38)
[Warning][Deadcode][CWE-571] condition '(int )p5_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:529:6-529:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode4 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:361:6-361: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:365:7-365:38)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:168:6-168: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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:572:6-572:20)
[Warning][Deadcode][CWE-571] condition '! ((int )mode5 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:375:6-375:19)
[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.5.1.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c:574:6-574: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
