./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-pthread.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-pthread.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-pthread.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, pthread_mutex_lock, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top___0, newTop, d, oldTop, curr_alloc_idx
[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-pthread.i:712:1-715: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-pthread.i:698:1-711: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-pthread.i:699:19-699: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-pthread.i:693:1-697: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-pthread.i:695:5-695: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-pthread.i:695:36-695: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-pthread.i:695:5-695: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-pthread.i:696:7-696: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-pthread.i:696:7-696: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-pthread.i:700:2-700: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-pthread.i:701:5-701: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-pthread.i:701:5-701: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-pthread.i:704:3-704:23)
[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-pthread.i:705:3-705:25)
[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-pthread.i:706:3-706:15)
[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-pthread.i:707:3-707: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-pthread.i:708:3-708:15)
[Info][Witness] unassume invariant: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:709:3-709:27)
[Info][Witness] unassume invariant: top <= 64 && 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:713:24-713:46)
[Info][Witness] unassume invariant: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:713:108-713:130)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'assume_abort_if_not' has dead code:
  on line 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:4-4)
[Warning][Deadcode] Function 'main' has dead code:
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:720-720)
[Warning][Deadcode] Function 'thr1' has dead code:
  on line 714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:714-714)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 23
  dead: 3
  total lines: 26
[Warning][Race] Memory location memory[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:689:5-689: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-pthread.i:704:3-704:23)
  write with [region:{memory[?]}, lock:{m}] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3-704:23)
  write with [region:{memory[?]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:719:13-719:43]] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3-704:23)
  write with [region:{memory[?]}, lock:{m}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:719:13-719:43]] (conf. 110)  (exp: & memory[newTop]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3-704:23)
  write with [region:{memory[?]}, lock:{m}] (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3-707:28)
  write with [region:{memory[?]}, lock:{m}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:719:13-719:43]] (conf. 110)  (exp: & memory[newTop + 1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3-707:28)
[Warning][Deadcode][CWE-571] condition '! cond' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:3:6-3:11)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.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-pthread.i:713:9-713: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-pthread.i:719:8-719:9)
[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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700: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-pthread.i:700:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:700:2)
[Success][Witness] invariant confirmed: -1 == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:700:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:700:2)
[Success][Witness] invariant confirmed: oldTop == newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:700:2)
[Success][Witness] invariant confirmed: newTop == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:700:2)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695:2)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695: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-pthread.i:695: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-pthread.i:705: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-pthread.i:705: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-pthread.i:705: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-pthread.i:705:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:705:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:705:3)
[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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699: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-pthread.i:699:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:699:2)
[Warning][Witness] invariant unconfirmed: 0 <= oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Success][Witness] invariant confirmed: oldTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:707:3)
[Warning][Witness] invariant unconfirmed: 1 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:709:3)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:709:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:709:3)
[Success][Witness] invariant confirmed: top != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:709:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:711:1)
[Warning][Witness] invariant unconfirmed: 0 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:701:2)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:701: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-pthread.i:701: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-pthread.i:701: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-pthread.i:701: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-pthread.i:701:2)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:701:2)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:701:2)
[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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702: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-pthread.i:702:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:702:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:702:3)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704: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-pthread.i:704: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-pthread.i:704: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-pthread.i:704: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-pthread.i:704:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3)
[Success][Witness] invariant confirmed: d == 10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:704:3)
[Success][Witness] invariant confirmed: 1 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:696:7)
[Success][Witness] invariant confirmed: next_alloc_idx <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:696: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-pthread.i:696: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-pthread.i:696:7)
[Warning][Witness] invariant unconfirmed: 1 <= newTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:708:3)
[Success][Witness] invariant confirmed: newTop <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:708:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:708:3)
[Success][Witness] invariant confirmed: newTop != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:708:3)
[Success][Witness] invariant confirmed: 3 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:697:1)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:697: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-pthread.i:697:1)
[Warning][Witness] invariant unconfirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:713:48)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:713:48)
[Success][Witness] invariant confirmed: 65 <= next_alloc_idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695:36)
[Success][Witness] invariant confirmed: next_alloc_idx <= 66 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695:36)
[Success][Witness] invariant confirmed: *curr_alloc_idx == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695: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-pthread.i:695:36)
[Success][Witness] invariant confirmed: next_alloc_idx != -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:695:36)
[Warning][Witness] invariant unconfirmed: 0 <= top (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:706:3)
[Success][Witness] invariant confirmed: top <= 64 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:706: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-pthread.i:706: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-pthread.i:706: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-pthread.i:706: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-pthread.i:706:3)
[Success][Witness] invariant confirmed: -1 == oldTop (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:706:3)
[Success][Witness] invariant confirmed: 10 == d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:706:3)
[Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/37_stack_lock_p0_vs_concur-pthread.i:713:3)
[Info][Witness] witness validation summary:
  confirmed: 96
  unconfirmed: 13
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 109
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 1
  total memory locations: 3
