./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.3.1.ufo.BOUNDED-6.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.3.1.ufo.BOUNDED-6.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.3.1.ufo.BOUNDED-6.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, node2__m2___1, node3__m3___1, assert__arg, 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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:311:2-311:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:135-135)
  on line 153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:153-153)
  on line 171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:171-171)
  on line 196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:196-196)
  on line 214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:214-214)
  on line 277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:277-277)
  on line 295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:295-295)
  on line 384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:384-384)
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:463-463)
  on line 508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:508-508)
  on line 554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:554-554)
  on line 575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:575-575)
  on line 591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:591-591)
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:595-595)
  on line 631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:631-631)
  on line 655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:655-655)
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:680-680)
  on line 686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:686-686)
  on line 693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:693-693)
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:698-698)
  on line 704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:704-704)
  on line 710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:710-710)
  on line 715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:715-715)
  on line 723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:723-723)
  on line 728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:728-728)
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:736-736)
  on line 741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:741-741)
  on line 749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:749-749)
  on line 754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:754-754)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 242
  dead: 31 (2 in uncalled functions)
  total lines: 273
[Warning][Deadcode][CWE-571] condition '(int )send3 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:176:6-176: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:178:6-178:21)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 <= 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:192:9-192:51)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:194:7-194:20)
[Warning][Deadcode][CWE-571] condition '((int )st1 + (int )st2) + (int )st3 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:200:9-200:51)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:202:7-202: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:212:6-212:22)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:220:6-220:18)
[Warning][Deadcode][CWE-571] condition '! ((int )mode1 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:225:6-225: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:230:7-230:38)
[Warning][Deadcode][CWE-571] condition '! ((int )mode2 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:240:6-240: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:244:7-244: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:450:6-450: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:452:6-452:21)
[Warning][Deadcode][CWE-571] condition '! ((int )mode3 == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:254:6-254: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:258:7-258: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:495:6-495: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:497:6-497:21)
[Warning][Deadcode][CWE-570] condition '(int )r1 >= 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:275:7-275:20)
[Warning][Deadcode][CWE-571] condition '(int )r1 < 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:283:7-283:19)
[Warning][Deadcode][CWE-570] condition '(int )assert__arg___0 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:293:6-293:22)
[Warning][Deadcode][CWE-571] condition '(int )send1 != (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:541:6-541: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:543:6-543:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:119:6-119:19)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:128:6-128:18)
[Warning][Deadcode][CWE-570] condition '! ((int )mode1 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:133:6-133: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:140:6-140: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:142:6-142:21)
[Warning][Deadcode][CWE-571] condition '(int )assert__arg___2 == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:588:6-588:22)
[Warning][Deadcode][CWE-570] condition '! ((int )mode2 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:151:6-151: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:158:6-158: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.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:160:6-160:21)
[Warning][Deadcode][CWE-570] condition '! ((int )mode3 == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.3.1.ufo.BOUNDED-6.pals.c.v+nlh-reducer.c:169:6-169:19)
[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
