/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/egcd3-ll_valuebound100.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/egcd3-ll_valuebound100.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/egcd3-ll_valuebound100.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:50:17)
[Warning][Witness] couldn't locate invariant: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: b != 0LL (../plain/egcd3-ll_valuebound100.c:51:17)
[Warning][Witness] couldn't locate invariant: 0LL <= k (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: b != 0LL (../plain/egcd3-ll_valuebound100.c:52:17)
[Warning][Witness] couldn't locate invariant: 1LL <= d (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: b != 0LL (../plain/egcd3-ll_valuebound100.c:53:17)
[Warning][Witness] couldn't locate invariant: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:55:21)
[Warning][Witness] couldn't locate invariant: 1LL <= d (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: c - 2LL * v >= 0LL (../plain/egcd3-ll_valuebound100.c:57:17)
[Warning][Witness] couldn't locate invariant: 2LL <= d (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: -2LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: c - 2LL * v >= 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: b != 0LL (../plain/egcd3-ll_valuebound100.c:58:17)
[Warning][Witness] couldn't locate invariant: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: (-1LL - c) + 2LL * v >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:60:13)
[Warning][Witness] couldn't locate invariant: -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: 0LL <= k (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: 1LL <= d (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: c <= 2147483646LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: c >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: ((0LL - b) + c) + v >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: (-1LL - c) + v >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: (a - c) - v >= 0LL (../plain/egcd3-ll_valuebound100.c:61:13)
[Warning][Witness] couldn't locate invariant: -9223372036854775805LL <= b (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: (-1LL + b) - c >= 0LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: b != 0LL (../plain/egcd3-ll_valuebound100.c:64:9)
[Warning][Witness] couldn't locate invariant: -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: -9223372036854775805LL <= a (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: c <= 2147483646LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - c) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - c >= 0LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: a != 0LL (../plain/egcd3-ll_valuebound100.c:65:9)
[Warning][Witness] couldn't locate invariant: -9223372036854775806LL <= b (../plain/egcd3-ll_valuebound100.c:67:9)
[Warning][Witness] couldn't locate invariant: b <= 2147483646LL (../plain/egcd3-ll_valuebound100.c:67:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:67:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:67:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:67:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:68:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:68:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:68:9)
[Warning][Witness] couldn't locate invariant: 0LL <= k (../plain/egcd3-ll_valuebound100.c:69:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:69:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:69:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:69:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:70:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:70:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:70:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:71:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:71:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:71:9)
[Warning][Witness] couldn't locate invariant: 0LL <= k (../plain/egcd3-ll_valuebound100.c:72:9)
[Warning][Witness] couldn't locate invariant: k >= 0LL (../plain/egcd3-ll_valuebound100.c:72:9)
[Warning][Witness] couldn't locate invariant: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:72:9)
[Warning][Witness] couldn't locate invariant: (-1LL + a) - b >= 0LL (../plain/egcd3-ll_valuebound100.c:72:9)
[Warning][Witness] couldn't locate invariant: -9223372036854775805LL <= a (../plain/egcd3-ll_valuebound100.c:74:5)
[Warning][Witness] couldn't locate invariant: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:74:5)
[Warning][Witness] couldn't locate invariant: ((0LL - a) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:74:5)
[Warning][Witness] couldn't locate invariant: ((0LL - a) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:75:5)
[Info][Witness] unassume invariant: ((((((((((((((0LL - a) - b) + (long long )x) + (long long )y >= 0LL && b <= 2147483647LL) && a <= 2147483647LL) && -9223372036854775805LL <= a) && -9223372036854775806LL <= b) && (long long )x >= 0LL) && 0 <= x) && b <= 2147483647LL) && (-0x7FFFFFFF-1) <= b) && a <= 2147483647LL) && (-0x7FFFFFFF-1) <= a) && (long long )y >= 0LL) && 0 <= y (../plain/egcd3-ll_valuebound100.c:33:5-33:10)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:55:21-55:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll_valuebound100.c:57:17-57:26)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:58:17-58:26)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((b != 0LL && c - v >= 0LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && -1LL + d >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && a <= 2147483647LL) && 1LL <= d) && 0LL <= k) && b != 0LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && b <= 2147483647LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && b != 0LL) && a - c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:58:17-58:26)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((b != 0LL && c - v >= 0LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && -1LL + d >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && a <= 2147483647LL) && 1LL <= d) && 0LL <= k) && b != 0LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && b <= 2147483647LL) && a - c >= 0LL) && (0LL - b) + c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && b != 0LL) && a - c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:47:13-47:18)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:50:17-50:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:51:17-51:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:52:17-52:50)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:53:17-53:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll_valuebound100.c:61:13-61:22)
[Info][Witness] unassume invariant: ((((((((((((((((b != 0LL && a - c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && a <= 2147483647LL) && 0LL <= k) && -9223372036854775806LL <= c) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && c <= 2147483647LL) && -9223372036854775805LL <= c) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && a <= 2147483647LL) && -9223372036854775805LL <= a) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && b <= 2147483647LL) && -9223372036854775806LL <= b (../plain/egcd3-ll_valuebound100.c:61:13-61:22)
[Info][Witness] unassume invariant: ((((((((((((((((b != 0LL && a - c >= 0LL) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && k >= 0LL) && c <= 2147483647LL) && b <= 2147483647LL) && a <= 2147483647LL) && 0LL <= k) && -9223372036854775806LL <= c) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && c <= 2147483647LL) && -9223372036854775805LL <= c) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && a <= 2147483647LL) && -9223372036854775805LL <= a) && (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL) && b <= 2147483647LL) && -9223372036854775806LL <= b (../plain/egcd3-ll_valuebound100.c:40:9-40:14)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:69:9-69:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:72:9-72:25)
[Info][Witness] unassume invariant: ((((((((((((((0LL - a) - b) + (long long )x) + (long long )y >= 0LL && b <= 2147483647LL) && a <= 2147483647LL) && -9223372036854775805LL <= a) && -9223372036854775806LL <= b) && (long long )x >= 0LL) && 0 <= x) && b <= 2147483647LL) && (-0x7FFFFFFF-1) <= b) && a <= 2147483647LL) && (-0x7FFFFFFF-1) <= a) && (long long )y >= 0LL) && 0 <= y (../plain/egcd3-ll_valuebound100.c:72:9-72:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll_valuebound100.c:74:5-74:50)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 50
  dead: 0
  total lines: 50
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound100.c:35:12-35:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound100.c:42:16-42:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll_valuebound100.c:49:20-49:21)
[Warning][Witness] invariant unconfirmed: 0 <= y (../plain/egcd3-ll_valuebound100.c:24:5)
[Warning][Witness] invariant unconfirmed: (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:24:5)
[Warning][Witness] invariant unconfirmed: (-0x7FFFFFFF-1) <= a (../plain/egcd3-ll_valuebound100.c:29:5)
[Success][Witness] invariant confirmed: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:29:5)
[Warning][Witness] invariant unconfirmed: (-0x7FFFFFFF-1) <= b (../plain/egcd3-ll_valuebound100.c:30:5)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:30:5)
[Warning][Witness] invariant unconfirmed: -9223372036854775806LL <= b (../plain/egcd3-ll_valuebound100.c:36:13)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:36:13)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:36:13)
[Warning][Witness] invariant unconfirmed: -9223372036854775805LL <= a (../plain/egcd3-ll_valuebound100.c:39:9)
[Success][Witness] invariant confirmed: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:39:9)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:39:9)
[Warning][Witness] invariant unconfirmed: -9223372036854775805LL <= c (../plain/egcd3-ll_valuebound100.c:40:9)
[Success][Witness] invariant confirmed: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:40:9)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:40:9)
[Success][Witness] invariant confirmed: -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: k >= 0LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow
[Success][Witness] invariant confirmed: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: b != 0LL (../plain/egcd3-ll_valuebound100.c:43:17)
[Success][Witness] invariant confirmed: k >= 0LL (../plain/egcd3-ll_valuebound100.c:46:13)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:46:13)
[Success][Witness] invariant confirmed: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:46:13)
[Success][Witness] invariant confirmed: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:46:13)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Success][Witness] invariant confirmed: k >= 0LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Success][Witness] invariant confirmed: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Success][Witness] invariant confirmed: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Success][Witness] invariant confirmed: b != 0LL (../plain/egcd3-ll_valuebound100.c:47:13)
[Warning][Witness] invariant unconfirmed: 0 <= x (../plain/egcd3-ll_valuebound100.c:22:5)
[Warning][Witness] invariant unconfirmed: (long long )x >= 0LL (../plain/egcd3-ll_valuebound100.c:22:5)
[Success][Witness] invariant confirmed: -9223372036854775806LL <= b (../plain/egcd3-ll_valuebound100.c:35:12)
[Success][Witness] invariant confirmed: -9223372036854775805LL <= a (../plain/egcd3-ll_valuebound100.c:35:12)
[Success][Witness] invariant confirmed: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:35:12)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:35:12)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:35:12)
[Success][Witness] invariant confirmed: -9223372036854775806LL <= c (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: 0LL <= k (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: k >= 0LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: b != 0LL (../plain/egcd3-ll_valuebound100.c:42:16)
[Success][Witness] invariant confirmed: 0LL <= k (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: 1LL <= d (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: a <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: b <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: c <= 2147483647LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: k >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: -1LL + d >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: (0LL - b) + c >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: a - c >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: c - v >= 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Success][Witness] invariant confirmed: b != 0LL (../plain/egcd3-ll_valuebound100.c:49:20)
[Info][Witness] witness validation summary:
  confirmed: 51
  unconfirmed: 9
  refuted: 0
  error: 120
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 180
SV-COMP result: unknown

vars = 105    evals = 619    narrow_reuses = 26

Timings:
                                  cputime   walltime   allocated   count
Default                            0.980s     0.980s    583.36MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.20MB      4×
  Cabs2cil                           0.005s     0.005s      4.89MB      4×
  mergeCIL                           0.003s     0.003s      3.36MB      1×
  analysis                           0.938s     0.939s    565.85MB      1×
    createCFG                          0.001s     0.001s      0.71MB      1×
      handle                             0.001s     0.001s      0.13MB     34×
      iter_connect                       0.001s     0.001s      0.46MB     34×
        computeSCCs                        0.001s     0.001s      0.28MB     35×
    FrontC                             0.003s     0.003s      0.86MB    120×
    Cabs2cil                           0.018s     0.019s     11.20MB    120×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.800s     0.800s    404.79MB      1×
      S.Dom.equal                        0.001s     0.002s      0.22MB    645×
      base unassume                      0.118s     0.119s    140.49MB     81×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.052s     0.052s     23.80MB      1×
        postsolver_iter                    0.052s     0.052s     23.71MB      1×
    warn_global                        0.001s     0.001s      0.26MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
