/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 graves-cpa/egcd3-ll.yml.witness.yml --witness.yaml.validate graves-cpa/egcd3-ll.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/egcd3-ll.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: (k == (0LL) && d == (1LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && d == (1LL) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) (../plain/egcd3-ll.c:50:17)
[Warning][Witness] couldn't locate invariant: (k == (0LL) && d == (1LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && d == (1LL) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) (../plain/egcd3-ll.c:51:17)
[Warning][Witness] couldn't locate invariant: (k == (0LL) && d == (1LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) || (k == (0LL) && (!(p == (0LL)) || (p == (0LL) && !(q == (1LL))) || (p == (0LL) && q == (1LL) && !(r == (1LL))) || (p == (0LL) && q == (1LL) && r == (1LL) && !(s == (0LL))) || (p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && !(temp == (0LL)))) && d == (1LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && !(d == (1LL)) && d == (2LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) (../plain/egcd3-ll.c:49:17)
[Info][Witness] unassume invariant: ((((((((temp == 0LL && r == 1LL) && p == 0LL) && q == 1LL) && k == 0LL) && s == 0LL) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && s == -1LL)) || ((((((! (temp == 0LL) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((((((((! (temp == 0LL) || (temp == 0LL && ! (r == 1LL))) || ((temp == 0LL && r == 1LL) && ! (p == 0LL))) || (((temp == 0LL && r == 1LL) && p == 0LL) && ! (q == 1LL))) || (((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && ! (d == 1LL))) || ((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && ! (k == 1LL))) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && ! (s == -1LL))) && (((((! (k == 0LL) || (k == 0LL && ! (p == 0LL))) || ((k == 0LL && p == 0LL) && ! (q == 1LL))) || (((k == 0LL && p == 0LL) && q == 1LL) && ! (r == 1LL))) || ((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == 0LL))) || (((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && ((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) || ((d == 1LL && k == 1LL) && ! (p == 0LL))) || (((d == 1LL && k == 1LL) && p == 0LL) && ! (q == 1LL))) || ((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && ! (r == 1LL))) || (((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == -1LL))) || ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) && ((((((((temp == 0LL && r == 1LL) && p == 0LL) && q == 1LL) && k == 0LL) && s == 0LL) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && s == -1LL)) || ((((((! (temp == 0LL) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((((((((! (temp == 0LL) || (temp == 0LL && ! (r == 1LL))) || ((temp == 0LL && r == 1LL) && ! (p == 0LL))) || (((temp == 0LL && r == 1LL) && p == 0LL) && ! (q == 1LL))) || (((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && ! (d == 1LL))) || ((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && ! (k == 1LL))) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && ! (s == -1LL))) && (((((! (k == 0LL) || (k == 0LL && ! (p == 0LL))) || ((k == 0LL && p == 0LL) && ! (q == 1LL))) || (((k == 0LL && p == 0LL) && q == 1LL) && ! (r == 1LL))) || ((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == 0LL))) || (((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && ((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) || ((d == 1LL && k == 1LL) && ! (p == 0LL))) || (((d == 1LL && k == 1LL) && p == 0LL) && ! (q == 1LL))) || ((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && ! (r == 1LL))) || (((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == -1LL))) || ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) (../plain/egcd3-ll.c:31:5-31:10)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:53:21-53:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll.c:55:17-55:26)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:56:17-56:26)
[Info][Witness] unassume invariant: ((((((((k == 0LL && d == 2LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 0LL && d == 2LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) && ((((((((k == 0LL && d == 2LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 0LL && d == 2LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) (../plain/egcd3-ll.c:56:17-56:26)
[Info][Witness] unassume invariant: ((((((((k == 0LL && d == 2LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 0LL && d == 2LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) && ((((((((k == 0LL && d == 2LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 0LL && d == 2LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (d == 2LL)) && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) (../plain/egcd3-ll.c:45:13-45:18)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:48:17-48:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:49:17-49:54)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:50:17-50:50)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:51:17-51:46)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:58:13-58:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/egcd3-ll.c:59:13-59:22)
[Info][Witness] unassume invariant: ((((((((((d == 1LL && k == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 1LL && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || (((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && (! (d == 1LL) || (d == 1LL && ! (k == 1LL)))) && ((((! (p == 0LL) || (p == 0LL && ! (q == 1LL))) || ((p == 0LL && q == 1LL) && ! (r == 1LL))) || (((p == 0LL && q == 1LL) && r == 1LL) && ! (s == 0LL))) || ((((p == 0LL && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (s == 0LL)) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && d == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL)) && (((((((((d == 1LL && k == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 1LL && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || (((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && (! (d == 1LL) || (d == 1LL && ! (k == 1LL)))) && ((((! (p == 0LL) || (p == 0LL && ! (q == 1LL))) || ((p == 0LL && q == 1LL) && ! (r == 1LL))) || (((p == 0LL && q == 1LL) && r == 1LL) && ! (s == 0LL))) || ((((p == 0LL && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (s == 0LL)) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && d == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL))) && ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL) (../plain/egcd3-ll.c:59:13-59:22)
[Info][Witness] unassume invariant: ((((((((((d == 1LL && k == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 1LL && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || (((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && (! (d == 1LL) || (d == 1LL && ! (k == 1LL)))) && ((((! (p == 0LL) || (p == 0LL && ! (q == 1LL))) || ((p == 0LL && q == 1LL) && ! (r == 1LL))) || (((p == 0LL && q == 1LL) && r == 1LL) && ! (s == 0LL))) || ((((p == 0LL && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (s == 0LL)) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && d == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL)) && (((((((((d == 1LL && k == 1LL) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL) || (((((((k == 1LL && d == 1LL) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || (((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((k == 0LL && (! (d == 1LL) || (d == 1LL && ! (k == 1LL)))) && ((((! (p == 0LL) || (p == 0LL && ! (q == 1LL))) || ((p == 0LL && q == 1LL) && ! (r == 1LL))) || (((p == 0LL && q == 1LL) && r == 1LL) && ! (s == 0LL))) || ((((p == 0LL && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) || ((((((((k == 0LL && ! (s == 0LL)) && (((! (p == 1LL) || (p == 1LL && ! (q == 0LL))) || ((p == 1LL && q == 0LL) && ! (r == 0LL))) || (((p == 1LL && q == 0LL) && r == 0LL) && ! (s == 1LL)))) && d == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL))) && ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && temp == 0LL) (../plain/egcd3-ll.c:38:9-38:14)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:67:9-67:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:70:9-70:25)
[Info][Witness] unassume invariant: ((((((((temp == 0LL && r == 1LL) && p == 0LL) && q == 1LL) && k == 0LL) && s == 0LL) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && s == -1LL)) || ((((((! (temp == 0LL) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((((((((! (temp == 0LL) || (temp == 0LL && ! (r == 1LL))) || ((temp == 0LL && r == 1LL) && ! (p == 0LL))) || (((temp == 0LL && r == 1LL) && p == 0LL) && ! (q == 1LL))) || (((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && ! (d == 1LL))) || ((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && ! (k == 1LL))) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && ! (s == -1LL))) && (((((! (k == 0LL) || (k == 0LL && ! (p == 0LL))) || ((k == 0LL && p == 0LL) && ! (q == 1LL))) || (((k == 0LL && p == 0LL) && q == 1LL) && ! (r == 1LL))) || ((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == 0LL))) || (((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && ((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) || ((d == 1LL && k == 1LL) && ! (p == 0LL))) || (((d == 1LL && k == 1LL) && p == 0LL) && ! (q == 1LL))) || ((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && ! (r == 1LL))) || (((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == -1LL))) || ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) && ((((((((temp == 0LL && r == 1LL) && p == 0LL) && q == 1LL) && k == 0LL) && s == 0LL) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && s == -1LL)) || ((((((! (temp == 0LL) && k == 0LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && temp == 0LL)) || ((((((((((((! (temp == 0LL) || (temp == 0LL && ! (r == 1LL))) || ((temp == 0LL && r == 1LL) && ! (p == 0LL))) || (((temp == 0LL && r == 1LL) && p == 0LL) && ! (q == 1LL))) || (((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && ! (d == 1LL))) || ((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && ! (k == 1LL))) || (((((((temp == 0LL && r == 1LL) && q == 1LL) && p == 0LL) && (! (k == 0LL) || (k == 0LL && ! (s == 0LL)))) && d == 1LL) && k == 1LL) && ! (s == -1LL))) && (((((! (k == 0LL) || (k == 0LL && ! (p == 0LL))) || ((k == 0LL && p == 0LL) && ! (q == 1LL))) || (((k == 0LL && p == 0LL) && q == 1LL) && ! (r == 1LL))) || ((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == 0LL))) || (((((k == 0LL && p == 0LL) && q == 1LL) && r == 1LL) && s == 0LL) && ! (temp == 0LL)))) && ((((((! (d == 1LL) || (d == 1LL && ! (k == 1LL))) || ((d == 1LL && k == 1LL) && ! (p == 0LL))) || (((d == 1LL && k == 1LL) && p == 0LL) && ! (q == 1LL))) || ((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && ! (r == 1LL))) || (((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && ! (s == -1LL))) || ((((((d == 1LL && k == 1LL) && p == 0LL) && q == 1LL) && r == 1LL) && s == -1LL) && ! (temp == 0LL)))) && p == 1LL) && q == 0LL) && r == 0LL) && s == 1LL)) (../plain/egcd3-ll.c:70:9-70:25)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/egcd3-ll.c:72:5-72:50)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 48
  dead: 0
  total lines: 48
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll.c:33:12-33:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll.c:40:16-40:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (../plain/egcd3-ll.c:47:20-47:21)
[Warning][Witness] invariant unconfirmed: d == (1LL) && k == (1LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (-1LL) && temp == (0LL) (../plain/egcd3-ll.c:35:13)
[Warning][Witness] invariant unconfirmed: (temp == (0LL) && r == (1LL) && p == (0LL) && q == (1LL) && k == (0LL) && s == (0LL)) || (temp == (0LL) && r == (1LL) && q == (1LL) && p == (0LL) && (!(k == (0LL)) || (k == (0LL) && !(s == (0LL)))) && d == (1LL) && k == (1LL) && s == (-1LL)) || (!(temp == (0LL)) && k == (0LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) || ((!(temp == (0LL)) || (temp == (0LL) && !(r == (1LL))) || (temp == (0LL) && r == (1LL) && !(p == (0LL))) || (temp == (0LL) && r == (1LL) && p == (0LL) && !(q == (1LL))) || (temp == (0LL) && r == (1LL) && q == (1LL) && p == (0LL) && (!(k == (0LL)) || (k == (0LL) && !(s == (0LL)))) && !(d == (1LL))) || (temp == (0LL) && r == (1LL) && q == (1LL) && p == (0LL) && (!(k == (0LL)) || (k == (0LL) && !(s == (0LL)))) && d == (1LL) && !(k == (1LL))) || (temp == (0LL) && r == (1LL) && q == (1LL) && p == (0LL) && (!(k == (0LL)) || (k == (0LL) && !(s == (0LL)))) && d == (1LL) && k == (1LL) && !(s == (-1LL)))) && (!(k == (0LL)) || (k == (0LL) && !(p == (0LL))) || (k == (0LL) && p == (0LL) && !(q == (1LL))) || (k == (0LL) && p == (0LL) && q == (1LL) && !(r == (1LL))) || (k == (0LL) && p == (0LL) && q == (1LL) && r == (1LL) && !(s == (0LL))) || (k == (0LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && !(temp == (0LL)))) && (!(d == (1LL)) || (d == (1LL) && !(k == (1LL))) || (d == (1LL) && k == (1LL) && !(p == (0LL))) || (d == (1LL) && k == (1LL) && p == (0LL) && !(q == (1LL))) || (d == (1LL) && k == (1LL) && p == (0LL) && q == (1LL) && !(r == (1LL))) || (d == (1LL) && k == (1LL) && p == (0LL) && q == (1LL) && r == (1LL) && !(s == (-1LL))) || (d == (1LL) && k == (1LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (-1LL) && !(temp == (0LL)))) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) (../plain/egcd3-ll.c:33:5)
[Warning][Witness] invariant unconfirmed: (k == (0LL) && d == (2LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && d == (2LL) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) || (k == (0LL) && !(d == (2LL)) && d == (1LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && !(d == (2LL)) && d == (1LL) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) (../plain/egcd3-ll.c:47:13)
[Warning][Witness] invariant unconfirmed: (d == (1LL) && k == (1LL) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (1LL) && d == (1LL) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) || ((!(d == (1LL)) || (d == (1LL) && !(k == (1LL)))) && k == (0LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && temp == (0LL)) || (k == (0LL) && (!(d == (1LL)) || (d == (1LL) && !(k == (1LL)))) && (!(p == (0LL)) || (p == (0LL) && !(q == (1LL))) || (p == (0LL) && q == (1LL) && !(r == (1LL))) || (p == (0LL) && q == (1LL) && r == (1LL) && !(s == (0LL))) || (p == (0LL) && q == (1LL) && r == (1LL) && s == (0LL) && !(temp == (0LL)))) && p == (1LL) && q == (0LL) && r == (0LL) && s == (1LL)) || (k == (0LL) && !(s == (0LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL))) || (p == (1LL) && q == (0LL) && !(r == (0LL))) || (p == (1LL) && q == (0LL) && r == (0LL) && !(s == (1LL)))) && d == (1LL) && p == (0LL) && q == (1LL) && r == (1LL) && s == (-1LL) && temp == (0LL)) (../plain/egcd3-ll.c:40:9)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 7
  refuted: 0
  error: 3
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 10
SV-COMP result: unknown

vars = 97    evals = 568    narrow_reuses = 25

Timings:
                                  cputime   walltime   allocated   count
Default                            3.519s     3.525s    642.31MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.19MB      4×
  Cabs2cil                           0.006s     0.006s      4.86MB      4×
  mergeCIL                           0.004s     0.004s      3.35MB      1×
  analysis                           3.479s     3.485s    624.88MB      1×
    createCFG                          0.001s     0.001s      0.67MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.44MB     34×
        computeSCCs                        0.001s     0.001s      0.26MB     35×
    FrontC                             0.017s     0.018s      3.07MB     14×
    Cabs2cil                           0.005s     0.005s      4.23MB     14×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.899s     1.899s    559.10MB      1×
      S.Dom.equal                        0.001s     0.002s      0.20MB    593×
      base unassume                      0.283s     0.283s    274.68MB     77×
      cheap_full_reach                   0.001s     0.001s      0.04MB      1×
      postsolver                         0.033s     0.033s     19.15MB      1×
        postsolver_iter                    0.033s     0.033s     19.08MB      1×
    warn_global                        0.001s     0.001s      0.19MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
