./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/triangular-longest-2.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/triangular-longest-2.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/pthread/triangular-longest-2.i


--------------------------------------------------------------------------------


[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] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] __VERIFIER_atomic_begin, __VERIFIER_atomic_end, i___0, key, count, a, tmp, count, i___0, j___0, i___1, j___1, k, size, r, top, condI, condJ, k, k, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((4294967294LL - (long long )condI) - (long long )condJ >= 0LL && (4294967295LL + (long long )condI) - (long long )condJ >= 0LL) && (4294967295LL - (long long )condI) + (long long )condJ >= 0LL) && (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:711:1-725:1)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )condI) - (long long )condJ >= 0LL && (4294967295LL + (long long )condI) - (long long )condJ >= 0LL) && (4294967295LL - (long long )condI) + (long long )condJ >= 0LL) && (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:713:3-713:53)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:696:12-696:17)
[Info][Witness] unassume invariant: j % 2 == 0 && 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:697:5-697:30)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:698:5-698:14)
[Info][Witness] unassume invariant: i % 2 == 1 && 5 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:698:5-698:14)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:696:12-696:17)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )condI) - (long long )condJ >= 0LL && (4294967295LL + (long long )condI) - (long long )condJ >= 0LL) && (4294967295LL - (long long )condI) + (long long )condJ >= 0LL) && (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:714:3-714:53)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:704:12-704:17)
[Info][Witness] unassume invariant: i % 2 == 1 && 3 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:705:5-705:30)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:706:5-706:14)
[Info][Witness] unassume invariant: j % 2 == 0 && 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:706:5-706:14)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:704:12-704:17)
[Info][Witness] unassume invariant: ((((i % 2 == 1 && (4294967294LL - (long long )condI) - (long long )condJ >= 0LL) && (4294967295LL + (long long )condI) - (long long )condJ >= 0LL) && (4294967295LL - (long long )condI) + (long long )condJ >= 0LL) && (4294967296LL + (long long )condI) + (long long )condJ >= 0LL) && 3 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:715:3-715:28)
[Info][Witness] unassume invariant: ((condI == 0 || condI == 1) && condI <= 1) && 0 <= condI (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:7-716:29)
[Info][Witness] unassume invariant: j % 2 == 0 && 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:718:3-718:28)
[Info][Witness] unassume invariant: ((condJ == 0 || condJ == 1) && condJ <= 1) && 0 <= condJ (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:719:7-719:29)
[Info][Witness] unassume invariant: (((condJ == 0 || condJ == 1) && (condI == 0 || ((0 <= condI && condI <= 1) && (condI == 0 || condI == 1)))) && condJ <= 1) && 0 <= condJ (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:720:3-720:26)
[Info][Witness] unassume invariant: (((condJ == 0 || condJ == 1) && (condI == 0 || ((0 <= condI && condI <= 1) && (condI == 0 || condI == 1)))) && condJ <= 1) && 0 <= condJ (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:7-721:21)
[Info][Witness] unassume invariant: (((long long )condI - (long long )condJ >= 0LL && (0LL - (long long )condI) - (long long )condJ >= 0LL) && (long long )condI + (long long )condJ >= 0LL) && (0LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:7-721:21)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:63:1-67:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:68:1-72:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:73:1-77:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:78:1-82:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:83:1-87:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 25
  dead: 5 (5 in uncalled functions)
  total lines: 30
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:693:73-693:74)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:714:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:714:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:714:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:714:3)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:724:3)
[Success][Witness] invariant confirmed: (long long )condI + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:724:3)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:724:3)
[Success][Witness] invariant confirmed: (long long )condI - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:724:3)
[Success][Witness] invariant confirmed: 0 <= condJ (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:720:3)
[Success][Witness] invariant confirmed: condJ <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:720:3)
[Success][Witness] invariant confirmed: condJ == 0 || condJ == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:720:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:713:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:713:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:713:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:713:3)
[Success][Witness] invariant confirmed: 3 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:706:5)
[Warning][Witness] invariant unconfirmed: i % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:706:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:715:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:715:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:715:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:715:3)
[Success][Witness] invariant confirmed: 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:698:5)
[Success][Witness] invariant confirmed: j % 2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:698:5)
[Success][Witness] invariant confirmed: 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:719:3)
[Success][Witness] invariant confirmed: j % 2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:719:3)
[Success][Witness] invariant confirmed: 5 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:699:5)
[Warning][Witness] invariant unconfirmed: i % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:699:5)
[Success][Witness] invariant confirmed: 4 <= j (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:707:5)
[Success][Witness] invariant confirmed: j % 2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:707:5)
[Success][Witness] invariant confirmed: 3 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )condI) + (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )condI) - (long long )condJ >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Warning][Witness] invariant unconfirmed: i % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:716:3)
[Success][Witness] invariant confirmed: 0 <= condI (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:717:3)
[Success][Witness] invariant confirmed: condI <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:717:3)
[Success][Witness] invariant confirmed: condI == 0 || condI == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:717:3)
[Success][Witness] invariant confirmed: 0 <= condJ (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:3)
[Success][Witness] invariant confirmed: condJ <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:3)
[Success][Witness] invariant confirmed: condI == 0 || ((0 <= condI && condI <= 1) && (condI == 0 || condI == 1)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:3)
[Success][Witness] invariant confirmed: condJ == 0 || condJ == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:721:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:704:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-2.i:696:3)
[Info][Witness] witness validation summary:
  confirmed: 39
  unconfirmed: 5
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 44
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 0
  total memory locations: 2
