./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/queue_ok_longest.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/queue_ok_longest.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/queue_ok_longest.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, reach_error, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, id1, id2, tmp, tmp___0, i, tmp, tmp___0, tmp___1, i, value, q, x, q, x, q, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
<string>[1:7-12] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: 0 <= ((QType *)arg)->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Info][Witness] invariant has invalid syntax: 0 <= ((QType *)arg)->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:7-12] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: 0 <= ((QType *)arg)->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Info][Witness] invariant has invalid syntax: 0 <= ((QType *)arg)->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:2-7] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: ((QType *)arg)->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Info][Witness] invariant has invalid syntax: ((QType *)arg)->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:2-7] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: ((QType *)arg)->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Info][Witness] invariant has invalid syntax: ((QType *)arg)->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:7-12] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: 0 <= ((QType *)arg)->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] invariant has invalid syntax: 0 <= ((QType *)arg)->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
<string>[1:7-12] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: 0 <= ((QType *)arg)->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] invariant has invalid syntax: 0 <= ((QType *)arg)->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
<string>[1:2-7] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: ((QType *)arg)->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] invariant has invalid syntax: ((QType *)arg)->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
<string>[1:2-7] : syntax error
Parsing error
[Error][Witness] Frontc couldn't parse invariant: ((QType *)arg)->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] invariant has invalid syntax: ((QType *)arg)->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] unassume invariant: (int )enqueue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1045:3-1045:19)
[Info][Witness] unassume invariant: (int )dequeue_flag == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1046:3-1046:19)
[Info][Witness] unassume invariant: ((q->tail == 0 && q->head == 0) && q->amount == 0) && (unsigned long )q == (unsigned long )(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:952:1-957:1)
[Info][Witness] unassume invariant: (((q->tail == 0 && q->head == 0) && q->amount == 0) && (unsigned long )q == (unsigned long )(& queue)) && queue.head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:954:3-954:12)
[Info][Witness] unassume invariant: (((q->tail == 0 && q->head == 0) && q->amount == 0) && (unsigned long )q == (unsigned long )(& queue)) && queue.tail == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3-955:12)
[Info][Witness] unassume invariant: (unsigned long )q == (unsigned long )(& queue) && queue.amount == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3-956:14)
[Info][Witness] unassume invariant: (((((queue.head == 0 && queue.tail == 0) && q->amount == 0) && q->head == 0) && q->tail == 0) || (((((((0 <= queue.head && 0 <= queue.tail) && 0 <= q->head) && 0 <= q->tail) && queue.head <= 800) && queue.tail <= 800) && q->head <= 800) && q->tail <= 800)) && (unsigned long )q == (unsigned long )(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:958:1-967:1)
[Info][Witness] unassume invariant: (unsigned long )q == (unsigned long )(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:960:7-960:25)
[Info][Witness] unassume invariant: (unsigned long )q == (unsigned long )(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:962:5-962:31)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )i) - (long long )value >= 0LL && (4294967295LL + (long long )i) - (long long )value >= 0LL) && (4294967295LL - (long long )i) + (long long )value >= 0LL) && (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1005:1-1022:1)
[Info][Witness] unassume invariant: (((((int )enqueue_flag == 0 || (int )enqueue_flag == 1) && (4294967294LL - (long long )i) - (long long )value >= 0LL) && (4294967295LL + (long long )i) - (long long )value >= 0LL) && (4294967295LL - (long long )i) + (long long )value >= 0LL) && (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1008:3-1008:25)
[Info][Witness] unassume invariant: (int )dequeue_flag == 0 || (int )dequeue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:7-1009:19)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )i) - (long long )value >= 0LL && (4294967295LL + (long long )i) - (long long )value >= 0LL) && (4294967295LL - (long long )i) + (long long )value >= 0LL) && (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:7-1009:19)
[Info][Witness] unassume invariant: (((((((((int )dequeue_flag == 0 || (int )dequeue_flag == 1) && (unsigned long )arg == (unsigned long )((void *)(& queue))) && (int )enqueue_flag == 1) && i <= 800) && queue.tail <= 800) && queue.head <= 800) && 0 <= i) && 0 <= queue.tail) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:8-1011:26)
[Info][Witness] unassume invariant: ((((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && queue.tail <= 800) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:978:1-991:1)
[Info][Witness] unassume invariant: ((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && 0 <= q->tail) && 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3-980:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3-981:14)
[Info][Witness] unassume invariant: ((((((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && queue.tail <= 800) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.tail) && -2147483647 <= q->amount) && -2147483647 <= queue.amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3-981:14)
[Info][Witness] unassume invariant: ((((q->tail == 800 && (unsigned long )q == (unsigned long )(& queue)) && queue.tail == 800) && q->head <= 800) && 0 <= q->head) && -2147483647 <= q->amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:7-982:23)
[Info][Witness] unassume invariant: ((queue.tail != 801 && (unsigned long )q == (unsigned long )(& queue)) && queue.tail <= 800) && 1 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5-984:16)
[Info][Witness] unassume invariant: ((((((((q->tail != 800 && queue.tail != 800) && (unsigned long )q == (unsigned long )(& queue)) && q->tail <= 799) && q->head <= 800) && queue.tail <= 799) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.tail) && -2147483647 <= q->amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:7-982:23)
[Info][Witness] unassume invariant: ((queue.tail != 801 && (unsigned long )q == (unsigned long )(& queue)) && queue.tail <= 800) && 1 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5-988:14)
[Info][Witness] unassume invariant: i <= 799 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1014:7-1014:28)
[Info][Witness] unassume invariant: (((((((((int )dequeue_flag == 0 || (int )dequeue_flag == 1) && (unsigned long )arg == (unsigned long )((void *)(& queue))) && (int )enqueue_flag == 1) && i <= 800) && queue.tail <= 800) && queue.head <= 800) && 0 <= i) && 0 <= queue.tail) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:8-1011:26)
[Info][Witness] unassume invariant: (int )enqueue_flag == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1017:5-1017:21)
[Info][Witness] unassume invariant: (int )dequeue_flag == 0 || (int )dequeue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1018:5-1018:21)
[Info][Witness] unassume invariant: (int )dequeue_flag == 0 || (int )dequeue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1026:3-1026:25)
[Info][Witness] unassume invariant: (int )enqueue_flag == 0 || (int )enqueue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1027:7-1027:19)
[Info][Witness] unassume invariant: (((((((((int )enqueue_flag == 0 || (int )enqueue_flag == 1) && (unsigned long )arg == (unsigned long )((void *)(& queue))) && (int )dequeue_flag == 1) && i <= 800) && queue.tail <= 800) && queue.head <= 800) && 0 <= i) && 0 <= queue.tail) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:8-1029:26)
[Info][Witness] unassume invariant: ((((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && queue.head <= 800) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:992:1-1004:1)
[Info][Witness] unassume invariant: ((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && 0 <= q->tail) && 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3-995:26)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3-996:14)
[Info][Witness] unassume invariant: ((((((((unsigned long )q == (unsigned long )(& queue) && q->tail <= 800) && q->head <= 800) && q->amount <= 2147483646) && queue.head <= 800) && queue.amount <= 2147483646) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3-996:14)
[Info][Witness] unassume invariant: ((((q->head == 800 && (unsigned long )q == (unsigned long )(& queue)) && queue.head == 800) && q->tail <= 800) && q->amount <= 2147483646) && 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:7-997:23)
[Info][Witness] unassume invariant: ((queue.head != 801 && (unsigned long )q == (unsigned long )(& queue)) && queue.head <= 800) && 1 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5-999:16)
[Info][Witness] unassume invariant: ((((((((q->head != 800 && queue.head != 800) && (unsigned long )q == (unsigned long )(& queue)) && q->tail <= 800) && q->head <= 799) && q->amount <= 2147483646) && queue.head <= 799) && 0 <= q->tail) && 0 <= q->head) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:7-997:23)
[Info][Witness] unassume invariant: ((queue.head != 801 && (unsigned long )q == (unsigned long )(& queue)) && queue.head <= 800) && 1 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5-1002:14)
[Info][Witness] unassume invariant: (((((((((int )enqueue_flag == 0 || (int )enqueue_flag == 1) && (unsigned long )arg == (unsigned long )((void *)(& queue))) && (int )dequeue_flag == 1) && i <= 800) && queue.tail <= 800) && queue.head <= 800) && 0 <= i) && 0 <= queue.tail) && 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:8-1029:26)
[Info][Witness] unassume invariant: (int )dequeue_flag == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1036:5-1036:21)
[Info][Witness] unassume invariant: (int )enqueue_flag == 0 || (int )enqueue_flag == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1037:5-1037:21)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:76:1-80:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:81:1-85:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:86:1-90:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:91:1-95:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:96:1-100:1)
[Warning][Deadcode] Function 'full' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:968:1-977:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1049-1049)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 59
  dead: 10 (9 in uncalled functions)
  total lines: 69
[Warning][Deadcode][CWE-570] condition 'tmp___0 == -1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1048:7-1048:27)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:21:73-21:74)
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)0 || dequeue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1020:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1008:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1008:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1008:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1008:3)
[Success][Witness] invariant confirmed: queue.tail == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3)
[Success][Witness] invariant confirmed: q->amount == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3)
[Success][Witness] invariant confirmed: q->head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3)
[Success][Witness] invariant confirmed: q->tail == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:956:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: q->amount <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: queue.head == 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: q->head == 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:999:5)
[Success][Witness] invariant confirmed: queue.head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3)
[Success][Witness] invariant confirmed: q->amount == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3)
[Success][Witness] invariant confirmed: q->head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3)
[Success][Witness] invariant confirmed: q->tail == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:955:3)
[Success][Witness] invariant confirmed: 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: queue.tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:980:3)
[Success][Witness] invariant confirmed: 1 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:990:3)
[Success][Witness] invariant confirmed: queue.tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:990:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:990:3)
[Success][Witness] invariant confirmed: queue.tail != 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:990:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:962:5)
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1018:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:960:3)
[Success][Witness] invariant confirmed: ((((queue.head == 0 && queue.tail == 0) && q->amount == 0) && q->head == 0) && q->tail == 0) || (((((((0 <= queue.head && 0 <= queue.tail) && 0 <= q->head) && 0 <= q->tail) && queue.head <= 800) && queue.tail <= 800) && q->head <= 800) && q->tail <= 800) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:960:3)
[Success][Witness] invariant confirmed: -2147483647 <= queue.amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: -2147483647 <= q->amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: queue.tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:982:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:3)
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)0 || enqueue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1009:3)
[Success][Witness] invariant confirmed: -2147483647 <= q->amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: queue.tail == 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: q->tail == 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:984:5)
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1047:3)
[Success][Witness] invariant confirmed: queue.amount == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:957:1)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:957:1)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:996:3)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:981:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:954:3)
[Success][Witness] invariant confirmed: q->amount == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:954:3)
[Success][Witness] invariant confirmed: q->head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:954:3)
[Success][Witness] invariant confirmed: q->tail == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:954:3)
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1037:5)
[Success][Witness] invariant confirmed: -2147483647 <= q->amount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: queue.tail <= 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: q->tail <= 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: queue.tail != 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: q->tail != 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:988:5)
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)0 || dequeue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1027:3)
[Success][Witness] invariant confirmed: 1 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1003:3)
[Success][Witness] invariant confirmed: queue.head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1003:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1003:3)
[Success][Witness] invariant confirmed: queue.head != 801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1003:3)
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)0 || enqueue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1039:3)
[Success][Witness] invariant confirmed: 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: queue.head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:995:3)
[Success][Witness] invariant confirmed: 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: queue.head <= 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q->amount <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q->head <= 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: queue.head != 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q->head != 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1002:5)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:963:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )i) + (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )i) - (long long )value >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1015:7)
[Success][Witness] invariant confirmed: i <= 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1015:7)
[Success][Witness] invariant confirmed: 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: 0 <= q->head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: 0 <= q->tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: queue.amount <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: queue.head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: q->amount <= 2147483646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: q->head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: q->tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:997:3)
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1046:3)
[Success][Witness] invariant confirmed: q == & queue (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:966:5)
[Success][Witness] invariant confirmed: 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:7-12] : syntax error
Parsing error
<string>[1:7-12] : syntax error
Parsing error
[Success][Witness] invariant confirmed: queue.head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: queue.tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: i <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
<string>[1:2-7] : syntax error
Parsing error
<string>[1:2-7] : syntax error
Parsing error
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: arg == (void *)(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)0 || enqueue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1029:5)
[Success][Witness] invariant confirmed: 0 <= queue.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: 0 <= queue.tail (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
<string>[1:7-12] : syntax error
Parsing error
<string>[1:7-12] : syntax error
Parsing error
[Success][Witness] invariant confirmed: queue.head <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: queue.tail <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: i <= 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
<string>[1:2-7] : syntax error
Parsing error
<string>[1:2-7] : syntax error
Parsing error
[Success][Witness] invariant confirmed: enqueue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: arg == (void *)(& queue) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Success][Witness] invariant confirmed: dequeue_flag == (_Bool)0 || dequeue_flag == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok_longest.i:1011:5)
[Info][Witness] witness validation summary:
  confirmed: 143
  unconfirmed: 0
  refuted: 0
  error: 8
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 151
SV-COMP result: ERROR (witness error)
[Info][Race] Memory locations race summary:
  safe: 7
  vulnerable: 0
  unsafe: 0
  total memory locations: 7
