./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/chl-chromosome-trans.wvr.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/chl-chromosome-trans.wvr.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/weaver/chl-chromosome-trans.wvr.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] assume_abort_if_not, pthread_create, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, b, a, tmp, tmp___0, size, i, arr, t1, t2, t3, tmp, i, stop, i, stop, i, stop
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: ((((size == 5 && 5 == size) && (2147483652LL - (long long )i) - (long long )size >= 0LL) && (2147483653LL + (long long )i) - (long long )size >= 0LL) && (2147483642LL - (long long )i) + (long long )size >= 0LL) && (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:114:1-123:1)
[Info][Witness] unassume invariant: ((((size == 5 && 5 == size) && (2147483652LL - (long long )i) - (long long )size >= 0LL) && (2147483653LL + (long long )i) - (long long )size >= 0LL) && (2147483642LL - (long long )i) + (long long )size >= 0LL) && (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3-115:33)
[Info][Witness] unassume invariant: ((((size == 5 && 5 == size) && (2147483652LL - (long long )i) - (long long )size >= 0LL) && (2147483653LL + (long long )i) - (long long )size >= 0LL) && (2147483642LL - (long long )i) + (long long )size >= 0LL) && (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3-116:69)
[Info][Witness] unassume invariant: (((5 == size && (2147483652LL - (long long )i) - (long long )size >= 0LL) && (2147483653LL + (long long )i) - (long long )size >= 0LL) && (2147483642LL - (long long )i) + (long long )size >= 0LL) && (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:6-118:54)
[Info][Witness] unassume invariant: (((((((((((((size == 5 && (int )isNull_5 == 0) && (int )isNull_3 == 0) && (int )isNull_1 == 0) && result_13 == 0) && result_10 == 0) && result_7 == 0) && (unsigned long )o_4 == (unsigned long )((int *)0)) && 5 == size) && (10LL - (long long )i) - (long long )size >= 0LL) && (5LL + (long long )i) - (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (-5LL + (long long )i) + (long long )size >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:12-119:17)
[Info][Witness] unassume invariant: (((((5 == size && (9LL - (long long )i) - (long long )size >= 0LL) && (5LL + (long long )i) - (long long )size >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && (-5LL + (long long )i) + (long long )size >= 0LL) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:7-119:32)
[Info][Witness] unassume invariant: (((((((((((((size == 5 && (int )isNull_5 == 0) && (int )isNull_3 == 0) && (int )isNull_1 == 0) && result_13 == 0) && result_10 == 0) && result_7 == 0) && (unsigned long )o_4 == (unsigned long )((int *)0)) && 5 == size) && (10LL - (long long )i) - (long long )size >= 0LL) && (5LL + (long long )i) - (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (-5LL + (long long )i) + (long long )size >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:12-119:17)
[Info][Witness] unassume invariant: (((5 == size && (long long )i - (long long )size >= 0LL) && (10LL - (long long )i) - (long long )size >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (-10LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:7-119:32)
[Info][Witness] unassume invariant: (int )isNull_1 == 0 || (int )isNull_1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:96:3-96:38)
[Info][Witness] unassume invariant: (int )isNull_3 == 0 || (int )isNull_3 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:97:3-97:38)
[Info][Witness] unassume invariant: (int )isNull_5 == 0 || (int )isNull_5 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:98:3-98:38)
[Info][Witness] unassume invariant: (((((int )isNull_1 == 0 || (int )isNull_1 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:48:1-60:1)
[Info][Witness] unassume invariant: (((((int )isNull_3 == 0 || (int )isNull_3 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3-49:33)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:9-50:24)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:52:7-52:12)
[Info][Witness] unassume invariant: i <= 4 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:10-53:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:127:3-127:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:128:10-128:15)
[Info][Witness] unassume invariant: (((int )stop == 0 || (int )stop == 1) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:55:5-55:27)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:56:5-56:8)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:10-53:22)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:10-53:22)
[Info][Witness] unassume invariant: (((((int )isNull_3 == 0 || (int )isNull_3 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:62:1-74:1)
[Info][Witness] unassume invariant: (((((int )isNull_5 == 0 || (int )isNull_5 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3-63:33)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:9-64:24)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:66:7-66:12)
[Info][Witness] unassume invariant: i <= 4 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:10-67:22)
[Info][Witness] unassume invariant: (((int )stop == 0 || (int )stop == 1) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:69:5-69:28)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:70:5-70:8)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:10-67:22)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:10-67:22)
[Info][Witness] unassume invariant: (((((int )isNull_1 == 0 || (int )isNull_1 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:76:1-88:1)
[Info][Witness] unassume invariant: (((((int )isNull_5 == 0 || (int )isNull_5 == 1) && (2147483648LL - (long long )i) - (long long )stop >= 0LL) && (2147483649LL + (long long )i) - (long long )stop >= 0LL) && (2147483647LL - (long long )i) + (long long )stop >= 0LL) && (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3-77:33)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:9-78:24)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:80:7-80:12)
[Info][Witness] unassume invariant: i <= 4 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:10-81:22)
[Info][Witness] unassume invariant: (((int )stop == 0 || (int )stop == 1) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:83:5-83:28)
[Info][Witness] unassume invariant: ((((int )stop == 0 || (int )stop == 1) && (unsigned long )_argptr == 0UL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:84:5-84:8)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:10-81:22)
[Info][Witness] unassume invariant: (int )stop == 0 || (int )stop == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:10-81:22)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:111-111)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 65
  dead: 1
  total lines: 66
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:70:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:70:5)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:70:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:82:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:82:5)
[Success][Witness] invariant confirmed: (-10LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:122:3)
[Success][Witness] invariant confirmed: (0LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:122:3)
[Success][Witness] invariant confirmed: (10LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:122:3)
[Success][Witness] invariant confirmed: (long long )i - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:122:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:122:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:118:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3)
[Success][Witness] invariant confirmed: isNull_3 == (_Bool)0 || isNull_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:63:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:3)
[Success][Witness] invariant confirmed: isNull_5 == (_Bool)0 || isNull_5 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:78:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:115:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:86:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:65:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:56:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:56:5)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:56:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:3)
[Success][Witness] invariant confirmed: isNull_5 == (_Bool)0 || isNull_5 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:64:3)
[Success][Witness] invariant confirmed: isNull_5 == (_Bool)0 || isNull_5 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:101:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:116:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:51:3)
[Success][Witness] invariant confirmed: isNull_3 == (_Bool)0 || isNull_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:98:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:68:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:68:5)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:8)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:8)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:8)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:8)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:8)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:58:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:72:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: (5LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: (9LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:120:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:54:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:54:5)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:79:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3)
[Success][Witness] invariant confirmed: isNull_1 == (_Bool)0 || isNull_1 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:77:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:3)
[Success][Witness] invariant confirmed: isNull_3 == (_Bool)0 || isNull_3 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )i) + (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )i) - (long long )stop >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3)
[Success][Witness] invariant confirmed: isNull_1 == (_Bool)0 || isNull_1 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:49:3)
[Success][Witness] invariant confirmed: isNull_1 == (_Bool)0 || isNull_1 == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:97:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:84:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:84:5)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:84:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: (0LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: (5LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: (10LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: o_4 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: result_7 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: result_10 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: result_13 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: isNull_1 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: isNull_3 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: isNull_5 == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:119:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:3)
[Success][Witness] invariant confirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:81:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:3)
[Success][Witness] invariant confirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:53:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:3)
[Success][Witness] invariant confirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:3)
[Success][Witness] invariant confirmed: stop == (_Bool)0 || stop == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-trans.wvr.c:67:3)
[Info][Witness] witness validation summary:
  confirmed: 116
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 116
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 10
  vulnerable: 0
  unsafe: 0
  total memory locations: 10
