./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/37_stack_lock_p0_vs_concur.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/37_stack_lock_p0_vs_concur.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-ext/37_stack_lock_p0_vs_concur.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] abort, assume_abort_if_not, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top___0, newTop, d, oldTop, curr_alloc_idx, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:725:1-733:1)
[Info][Witness] unassume invariant: (((((((((((10 == d && (4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL) && (2147483657LL - (long long )d) - (long long )newTop >= 0LL) && (2147483657LL - (long long )d) - (long long )oldTop >= 0LL) && (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL) && (2147483637LL + (long long )d) - (long long )newTop >= 0LL) && (2147483637LL + (long long )d) - (long long )oldTop >= 0LL) && (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL) && (2147483658LL - (long long )d) + (long long )newTop >= 0LL) && (2147483658LL - (long long )d) + (long long )oldTop >= 0LL) && (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL) && (2147483638LL + (long long )d) + (long long )newTop >= 0LL) && (2147483638LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:709:1-724:1)
[Info][Witness] unassume invariant: (((((((((((((((newTop == -1 && oldTop == newTop) && 10 == d) && -1 == newTop) && -1 == oldTop) && (long long )newTop - (long long )oldTop >= 0LL) && (9LL - (long long )d) - (long long )newTop >= 0LL) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-2LL - (long long )newTop) - (long long )oldTop >= 0LL) && (-11LL + (long long )d) - (long long )newTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )newTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (0LL - (long long )newTop) + (long long )oldTop >= 0LL) && (2LL + (long long )newTop) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )newTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:19-710:30)
[Info][Witness] unassume invariant: (next_alloc_idx % 2 == 1 && next_alloc_idx <= 66) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:704:1-708:1)
[Info][Witness] unassume invariant: (((next_alloc_idx != -1 && next_alloc_idx % 2 == 1) && *curr_alloc_idx == -1) && next_alloc_idx <= 66) && 65 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:5-706:34)
[Info][Witness] unassume invariant: (next_alloc_idx % 2 == 1 && next_alloc_idx <= 66) && 3 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36-706:55)
[Info][Witness] unassume invariant: (((((1 <= *curr_alloc_idx && *curr_alloc_idx <= 64) && *curr_alloc_idx % 2 == 1) || *curr_alloc_idx == -1) && next_alloc_idx % 2 == 1) && next_alloc_idx <= 64) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:5-706:34)
[Info][Witness] unassume invariant: (((((1 <= *curr_alloc_idx && *curr_alloc_idx <= 64) && *curr_alloc_idx % 2 == 1) || *curr_alloc_idx == -1) && next_alloc_idx % 2 == 1) && next_alloc_idx <= 64) && 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7-707:60)
[Info][Witness] unassume invariant: (next_alloc_idx % 2 == 1 && next_alloc_idx <= 66) && 3 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7-707:60)
[Info][Witness] unassume invariant: ((((((10 == d && -1 == oldTop) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL) && newTop <= 64) && 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2-711:41)
[Info][Witness] unassume invariant: ((((((((((((10 == d && -1 == oldTop) && (10LL - (long long )d) - (long long )newTop >= 0LL) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-1LL - (long long )newTop) - (long long )oldTop >= 0LL) && (-1LL + (long long )newTop) - (long long )oldTop >= 0LL) && (-10LL + (long long )d) - (long long )newTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (10LL - (long long )d) + (long long )newTop >= 0LL) && (1LL - (long long )newTop) + (long long )oldTop >= 0LL) && (1LL + (long long )newTop) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL) && (-10LL + (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:5-712:16)
[Info][Witness] unassume invariant: ((((((((newTop != 0 && d == 10) && 10 == d) && -1 == oldTop) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL) && newTop <= 64) && 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:5-712:16)
[Info][Witness] unassume invariant: ((((10 == d && -1 == oldTop) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3-715:23)
[Info][Witness] unassume invariant: ((m == 0 || m == 1) && m <= 1) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:694:1-698:1)
[Info][Witness] unassume invariant: m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:697:2-697:7)
[Info][Witness] unassume invariant: ((((((10 == d && -1 == oldTop) && (9LL - (long long )d) - (long long )oldTop >= 0LL) && (-11LL + (long long )d) - (long long )oldTop >= 0LL) && (11LL - (long long )d) + (long long )oldTop >= 0LL) && (-9LL + (long long )d) + (long long )oldTop >= 0LL) && top <= 64) && 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3-716:30)
[Info][Witness] unassume invariant: ((((newTop != 0 && 10 == d) && newTop <= 64) && oldTop <= 64) && 1 <= newTop) && 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3-717:15)
[Info][Witness] unassume invariant: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3-718:28)
[Info][Witness] unassume invariant: ((newTop != 0 && 10 == d) && newTop <= 64) && 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:719:3-719:28)
[Info][Witness] unassume invariant: ((top != 0 && 10 == d) && top <= 64) && 1 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3-720:15)
[Info][Witness] unassume invariant: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:721:3-721:26)
[Info][Witness] unassume invariant: ((m == 0 || m == 1) && m <= 1) && 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:699:1-703:1)
[Info][Witness] unassume invariant: m == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:702:2-702:7)
[Info][Witness] unassume invariant: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:722:3-722:30)
[Info][Witness] unassume invariant: top <= 64 && 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:728:5-728:30)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:730:5-730:28)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:73:1-77:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:78:1-82:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:83:1-87:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:88:1-92:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:93:1-97:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:738-738)
[Warning][Deadcode] Function 'thr1' has dead code:
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:732-732)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 38
  dead: 7 (5 in uncalled functions)
  total lines: 45
[Warning][Race] Memory location memory[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:690:5-690:21)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3-715:23)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:737:13-737:43]] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3-715:23)
  write with region:{memory[?]} (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3-718:28)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:737:13-737:43]] (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3-718:28)
[Warning][Race] Memory location top (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:693:5-693:12)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3-720:15)
  write with [region:{top}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:737:13-737:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3-720:15)
  read with region:{top} (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3-717:15)
  read with [region:{top}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:737:13-737:43]] (conf. 110)  (exp: & top) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3-717:15)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:16:73-16:74)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:726:9-726:10)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:737:8-737:9)
[Warning][Witness] invariant unconfirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Success][Witness] invariant confirmed: oldTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:718:3)
[Warning][Witness] invariant unconfirmed: 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:712:2)
[Success][Witness] invariant confirmed: 65 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36)
[Success][Witness] invariant confirmed: *curr_alloc_idx == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36)
[Success][Witness] invariant confirmed: next_alloc_idx != -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:36)
[Warning][Witness] invariant unconfirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:729:7)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:729:7)
[Success][Witness] invariant confirmed: (-10LL + (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (1LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (1LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (10LL - (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (-10LL + (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (-1LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (-1LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: (10LL - (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:713:3)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:2)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:2)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:706:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:724:1)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:719:3)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7)
[Success][Witness] invariant confirmed: next_alloc_idx <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7)
[Warning][Witness] invariant unconfirmed: ((1 <= *curr_alloc_idx && *curr_alloc_idx <= 64) && *curr_alloc_idx % 2 == 1) || *curr_alloc_idx == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:707:7)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:696:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:696:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:696:2)
[Success][Witness] invariant confirmed: m == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:703:1)
[Success][Witness] invariant confirmed: (2147483638LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483638LL + (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483658LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483658LL - (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483637LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483637LL + (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483657LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (2147483657LL - (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:710:2)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:716:3)
[Success][Witness] invariant confirmed: 3 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:708:1)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:708:1)
[Warning][Witness] invariant unconfirmed: next_alloc_idx % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:708:1)
[Success][Witness] invariant confirmed: 0 <= m (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:701:2)
[Success][Witness] invariant confirmed: m <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:701:2)
[Success][Witness] invariant confirmed: m == 0 || m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:701:2)
[Success][Witness] invariant confirmed: m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:698:1)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:720:3)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (2LL + (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (0LL - (long long )newTop) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (-2LL - (long long )newTop) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )newTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: (long long )newTop - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: -1 == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: oldTop == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Success][Witness] invariant confirmed: newTop == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:711:2)
[Warning][Witness] invariant unconfirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:717:3)
[Warning][Witness] invariant unconfirmed: 1 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:721:3)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:721:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:721:3)
[Success][Witness] invariant confirmed: top != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:721:3)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: (-9LL + (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: (11LL - (long long )d) + (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: (-11LL + (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: (9LL - (long long )d) - (long long )oldTop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: d == 10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:715:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:722:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur.i:726:3)
[Info][Witness] witness validation summary:
  confirmed: 106
  unconfirmed: 13
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 119
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 2
  total memory locations: 4
