./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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-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, node1__m1___0, node1__m1___1, node1__m1___2, node1__m1___3, node2__m2, node3__m3, 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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:264:2-264:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:397:2-397:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:530:2-530:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:663:2-663:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:799:2-799:28)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:18:1-20:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:269-269)
  on line 271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:271-271)
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:284-284)
  on line 286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:286-286)
  on line 299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:299-299)
  on line 301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:301-301)
  on line 314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:314-314)
  on line 316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:316-316)
  on line 329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:329-329)
  on line 331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:331-331)
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:344-344)
  on line 346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:346-346)
  on line 920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:920-920)
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1551-1551)
  on line 1863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1863-1863)
  on line 2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2175-2175)
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2216-2216)
  on line 2218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2218-2218)
  on line 2261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2261-2261)
  on line 2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2263-2263)
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2306-2306)
  on line 2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2308-2308)
  on line 2351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2351-2351)
  on line 2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2353-2353)
  on line 2396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2396-2396)
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2398-2398)
  on line 2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2441-2441)
  on line 2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2443-2443)
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2448-2448)
  on line 2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2487-2487)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 753
  dead: 32 (2 in uncalled functions)
  total lines: 785
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2327:6-2327:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2015:6-2015:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1703:6-1703:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1391:6-1391:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1078:6-1078:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:523:6-523:19)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2372:6-2372:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2060:6-2060:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1748:6-1748:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1436:6-1436:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1123:6-1123:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:390:6-390:19)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2417:6-2417:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2105:6-2105:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1793:6-1793:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1481:6-1481:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1168:6-1168:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2463:6-2463:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:257:6-257:19)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2151:6-2151:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1839:6-1839:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1527:6-1527:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1214:6-1214:21)
[Warning][Deadcode][CWE-570] condition '(int )node1__m1 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:267:7-267:38)
[Warning][Deadcode][CWE-570] condition '(int )node2__m2 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:282:7-282:38)
[Warning][Deadcode][CWE-570] condition '(int )node3__m3 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:297:7-297:38)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2237:6-2237:21)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1925:6-1925:21)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1613:6-1613:21)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1301:6-1301:21)
[Warning][Deadcode][CWE-571] condition '(int )p6_new == (int )nomsg' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:988:6-988:21)
[Warning][Deadcode][CWE-570] condition '(int )node4__m4 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:312:7-312: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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:2282:6-2282:21)
[Warning][Deadcode][CWE-570] condition '(int )node5__m5 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:327:7-327: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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1970:6-1970:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1658:6-1658:21)
[Warning][Deadcode][CWE-571] condition 'main__i2 < 12' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:656:6-656:19)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1346:6-1346:21)
[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.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:1033:6-1033:21)
[Warning][Deadcode][CWE-570] condition '(int )node6__m6 != (int )nomsg' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/seq-mthreaded-reduced/pals_lcr.6.1.ufo.BOUNDED-12.pals.c.p+lhb-reducer.c:342:7-342:38)
[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
