./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-opt-symm.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-opt-symm.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-opt-symm.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, size, i, arr, t1, t2, i, comp, tmp, i, comp, tmp
[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-opt-symm.wvr.c:98:1-107: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-opt-symm.wvr.c:99:3-99: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-opt-symm.wvr.c:100:3-100: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-opt-symm.wvr.c:102:6-102:54)
[Info][Witness] unassume invariant: (((((((((((size == 5 && isNullB == 0) && isNullA == 0) && res2 == 0) && res1 == 0) && (unsigned long )scoreB == (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-opt-symm.wvr.c:103:12-103: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-opt-symm.wvr.c:103:7-103:32)
[Info][Witness] unassume invariant: (((((((((((size == 5 && isNullB == 0) && isNullA == 0) && res2 == 0) && res1 == 0) && (unsigned long )scoreB == (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-opt-symm.wvr.c:103:12-103: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-opt-symm.wvr.c:103:7-103:32)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )comp) - (long long )i >= 0LL && (4294967295LL + (long long )comp) - (long long )i >= 0LL) && (4294967295LL - (long long )comp) + (long long )i >= 0LL) && (4294967296LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:46:1-60:1)
[Info][Witness] unassume invariant: ((((i == 0 && 0 == i) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:47:7-47:12)
[Info][Witness] unassume invariant: ((((((unsigned long )_argptr == 0UL && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3-49:36)
[Info][Witness] unassume invariant: (((((2147483647LL - (long long )comp) - (long long )i >= 0LL && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:10-50:31)
[Info][Witness] unassume invariant: (((((((((comp == -1 || comp == 0) || comp == 1) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5-51:72)
[Info][Witness] unassume invariant: (((((((((comp == -1 || comp == 0) || comp == 1) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5-51:72)
[Info][Witness] unassume invariant: (((((4LL - (long long )comp) - (long long )i >= 0LL && (4LL + (long long )comp) - (long long )i >= 0LL) && (long long )comp + (long long )i >= 0LL) && (0LL - (long long )comp) + (long long )i >= 0LL) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:9-52:18)
[Info][Witness] unassume invariant: ((((((unsigned long )_argptr == 0UL && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5-56:8)
[Info][Witness] unassume invariant: (((((((((res1 == -1 || res1 == 0) || res1 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res1 <= 127) && res1 <= 1) && -1 <= res1) && -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:10-50:31)
[Info][Witness] unassume invariant: (((((((((res1 == -1 || res1 == 0) || res1 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res1 <= 127) && res1 <= 1) && -1 <= res1) && -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:10-50:31)
[Info][Witness] unassume invariant: (((((((((((comp == -1 || comp == 1) && comp != 0) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && i <= 4) && 0 <= i) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:9-52:18)
[Info][Witness] unassume invariant: (((((((((res1 == -1 || res1 == 0) || res1 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res1 <= 127) && res1 <= 1) && -1 <= res1) && -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7-53:18)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )comp) - (long long )i >= 0LL && (4294967295LL + (long long )comp) - (long long )i >= 0LL) && (4294967295LL - (long long )comp) + (long long )i >= 0LL) && (4294967296LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:62:1-76:1)
[Info][Witness] unassume invariant: ((((i == 0 && 0 == i) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:63:7-63:12)
[Info][Witness] unassume invariant: ((((((unsigned long )_argptr == 0UL && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3-65:36)
[Info][Witness] unassume invariant: (((((2147483647LL - (long long )comp) - (long long )i >= 0LL && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:10-66:31)
[Info][Witness] unassume invariant: (((((((((comp == -1 || comp == 0) || comp == 1) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5-67:72)
[Info][Witness] unassume invariant: (((((((((comp == -1 || comp == 0) || comp == 1) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5-67:72)
[Info][Witness] unassume invariant: (((((4LL - (long long )comp) - (long long )i >= 0LL && (4LL + (long long )comp) - (long long )i >= 0LL) && (long long )comp + (long long )i >= 0LL) && (0LL - (long long )comp) + (long long )i >= 0LL) && i <= 4) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:9-68:18)
[Info][Witness] unassume invariant: ((((((unsigned long )_argptr == 0UL && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && i <= 5) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5-72:8)
[Info][Witness] unassume invariant: (((((((((res2 == -1 || res2 == 0) || res2 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res2 <= 127) && res2 <= 1) && -1 <= res2) && -128 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:10-66:31)
[Info][Witness] unassume invariant: (((((((((res2 == -1 || res2 == 0) || res2 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res2 <= 127) && res2 <= 1) && -1 <= res2) && -128 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:10-66:31)
[Info][Witness] unassume invariant: (((((((((((comp == -1 || comp == 1) && comp != 0) && (5LL - (long long )comp) - (long long )i >= 0LL) && (5LL + (long long )comp) - (long long )i >= 0LL) && (1LL - (long long )comp) + (long long )i >= 0LL) && (1LL + (long long )comp) + (long long )i >= 0LL) && comp <= 127) && comp <= 1) && i <= 4) && 0 <= i) && -1 <= comp) && -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:9-68:18)
[Info][Witness] unassume invariant: (((((((((res2 == -1 || res2 == 0) || res2 == 1) && (2147483647LL - (long long )comp) - (long long )i >= 0LL) && (2147483648LL + (long long )comp) - (long long )i >= 0LL) && (2147483647LL - (long long )comp) + (long long )i >= 0LL) && (2147483648LL + (long long )comp) + (long long )i >= 0LL) && res2 <= 127) && res2 <= 1) && -1 <= res2) && -128 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7-69:18)
[Info][Witness] unassume invariant: ((((((((((res2 == -1 || res2 == 0) || res2 == 1) && ((res1 == -1 || res1 == 0) || res1 == 1)) && res2 <= 127) && res2 <= 1) && res1 <= 127) && res1 <= 1) && -1 <= res2) && -1 <= res1) && -128 <= res2) && -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:90:3-90:22)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 95 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:95-95)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 41
  dead: 1
  total lines: 42
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:51:5)
[Success][Witness] invariant confirmed: -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: -1 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: comp <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: comp <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: (1LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: (1LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: (5LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: (5LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: comp != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Success][Witness] invariant confirmed: comp == -1 || comp == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:69:7)
[Warning][Witness] invariant unconfirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Warning][Witness] invariant unconfirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Warning][Witness] invariant unconfirmed: (long long )comp + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Warning][Witness] invariant unconfirmed: (4LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Warning][Witness] invariant unconfirmed: (4LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:72:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: (5LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: (9LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:104:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:63:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:63:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:63:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:63:3)
[Warning][Witness] invariant unconfirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Warning][Witness] invariant unconfirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Warning][Witness] invariant unconfirmed: (long long )comp + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Warning][Witness] invariant unconfirmed: (4LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Warning][Witness] invariant unconfirmed: (4LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:56:5)
[Success][Witness] invariant confirmed: -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: -1 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: comp <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: comp <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (1LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (1LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (5LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (5LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (comp == -1 || comp == 0) || comp == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:68:5)
[Success][Witness] invariant confirmed: (-10LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:106:3)
[Success][Witness] invariant confirmed: (0LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:106:3)
[Success][Witness] invariant confirmed: (10LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:106:3)
[Success][Witness] invariant confirmed: (long long )i - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:106:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:106:3)
[Success][Witness] invariant confirmed: -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: -128 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: -1 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: -1 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: res1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: res1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: res2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: res2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: (res1 == -1 || res1 == 0) || res1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: (res2 == -1 || res2 == 0) || res2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:92:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:99:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:67:5)
[Success][Witness] invariant confirmed: -128 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: -1 <= res1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: res1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: res1 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (res1 == -1 || res1 == 0) || res1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:59:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:8)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:8)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:8)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:8)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:8)
[Success][Witness] invariant confirmed: -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: -1 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: i <= 4 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: comp <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: comp <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: (1LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: (1LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: (5LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: (5LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: comp != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: comp == -1 || comp == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:53:7)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:47:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:47:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:47:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:47:3)
[Success][Witness] invariant confirmed: -128 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: -1 <= res2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: res2 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: res2 <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (res2 == -1 || res2 == 0) || res2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:75:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:102:3)
[Success][Witness] invariant confirmed: -128 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: -1 <= comp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: comp <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: comp <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (1LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (1LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (5LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (5LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (comp == -1 || comp == 0) || comp == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:52:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: 0 == i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: i == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:65:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: 0 == i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: i == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:49:3)
[Success][Witness] invariant confirmed: (2147483643LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: (2147483642LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: (2147483653LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: (2147483652LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:100:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Warning][Witness] invariant unconfirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:50:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: (0LL - (long long )i) + (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: (5LL + (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: (10LL - (long long )i) - (long long )size >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: 5 == size (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: scoreB == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: res1 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: res2 == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: isNullA == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: isNullB == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: size == 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:103:3)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Warning][Witness] invariant unconfirmed: i <= 5 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )comp) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Success][Witness] invariant confirmed: (unsigned long )_argptr == 0UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-chromosome-opt-symm.wvr.c:66:3)
[Info][Witness] witness validation summary:
  confirmed: 162
  unconfirmed: 14
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 176
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 7
  vulnerable: 0
  unsafe: 0
  total memory locations: 7
