/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/apache-get-tag.i.v+lhb-reducer.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/apache-get-tag.i.v+lhb-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/apache-get-tag.i.v+lhb-reducer.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: 0 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:286:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:286:6)
[Warning][Witness] couldn't locate invariant: (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:286:6)
[Warning][Witness] couldn't locate invariant: 0 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:287:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:288:6)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:288:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:288:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:288:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:288:6)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:292:2)
[Warning][Witness] couldn't locate invariant: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:292:2)
[Warning][Witness] couldn't locate invariant: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:292:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:292:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:304:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:328:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:340:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:340:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:340:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:340:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:340:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:361:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:373:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:373:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:373:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:373:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:373:2)
[Warning][Witness] couldn't locate invariant: 0LL - (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:400:2)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tagbuf_len != 0 && main__tagbuf_len != -1) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 1) && main__t != 0) && main__t != -1) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 2 <= main__t) && 2 <= main__tagbuf_len) && main__t != 1) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 2 <= main__t) && main__t != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 2 <= main__t) && 1 <= main__tagbuf_len) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__t >= 0LL) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__t >= 0LL) && main__t != 0) && main__t != -1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:283:2-283:40)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tagbuf_len != 0 && main__tagbuf_len != -1) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 1) && main__t != 0) && main__t != -1) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 2 <= main__t) && 2 <= main__tagbuf_len) && main__t != 1) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 2 <= main__t) && main__t != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 2 <= main__t) && 1 <= main__tagbuf_len) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && main__t != 0) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__t >= 0LL) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__t >= 0LL) && main__t != 0) && main__t != -1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:383:2-383:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.v+lhb-reducer.c:287:2-287:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.v+lhb-reducer.c:61:2-61:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((main__tagbuf_len != 0 && main__tagbuf_len != -1) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != -1) && (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__tagbuf_len != 0) && -1LL + (long long )main__tagbuf_len >= 0LL) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:61:2-61:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.v+lhb-reducer.c:132:2-132:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.v+lhb-reducer.c:194:2-194:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((main__tagbuf_len != 0 && main__tagbuf_len != -1) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != -1) && (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__tagbuf_len != 0) && -1LL + (long long )main__tagbuf_len >= 0LL) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__t) && 1 <= main__tagbuf_len) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 0 <= main__t) && (long long )main__t >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:194:2-194:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (../plain/apache-get-tag.i.v+lhb-reducer.c:4:1-4:96)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/apache-get-tag.i.v+lhb-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 41 (../plain/apache-get-tag.i.v+lhb-reducer.c:41-41)
  on lines 52..53 (../plain/apache-get-tag.i.v+lhb-reducer.c:52-53)
  on lines 72..73 (../plain/apache-get-tag.i.v+lhb-reducer.c:72-73)
  on lines 84..85 (../plain/apache-get-tag.i.v+lhb-reducer.c:84-85)
  on lines 114..115 (../plain/apache-get-tag.i.v+lhb-reducer.c:114-115)
  on lines 126..127 (../plain/apache-get-tag.i.v+lhb-reducer.c:126-127)
  on lines 142..143 (../plain/apache-get-tag.i.v+lhb-reducer.c:142-143)
  on lines 154..155 (../plain/apache-get-tag.i.v+lhb-reducer.c:154-155)
  on lines 176..177 (../plain/apache-get-tag.i.v+lhb-reducer.c:176-177)
  on lines 188..189 (../plain/apache-get-tag.i.v+lhb-reducer.c:188-189)
  on lines 224..225 (../plain/apache-get-tag.i.v+lhb-reducer.c:224-225)
  on lines 236..237 (../plain/apache-get-tag.i.v+lhb-reducer.c:236-237)
  on line 267 (../plain/apache-get-tag.i.v+lhb-reducer.c:267-267)
  on lines 278..279 (../plain/apache-get-tag.i.v+lhb-reducer.c:278-279)
  on lines 297..298 (../plain/apache-get-tag.i.v+lhb-reducer.c:297-298)
  on lines 309..310 (../plain/apache-get-tag.i.v+lhb-reducer.c:309-310)
  on lines 333..334 (../plain/apache-get-tag.i.v+lhb-reducer.c:333-334)
  on lines 345..346 (../plain/apache-get-tag.i.v+lhb-reducer.c:345-346)
  on lines 366..367 (../plain/apache-get-tag.i.v+lhb-reducer.c:366-367)
  on lines 378..379 (../plain/apache-get-tag.i.v+lhb-reducer.c:378-379)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 98
  dead: 41 (3 in uncalled functions)
  total lines: 139
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___0 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:50:6-50:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___13 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:295:6-295:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___14 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:307:6-307:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___1 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:70:6-70:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___15 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:331:6-331:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___2 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:82:6-82:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___16 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:343:6-343:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___17 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:364:6-364:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___3 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:112:6-112:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___18 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:376:6-376:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___4 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:124:6-124:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___5 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:140:6-140:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___6 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:152:6-152:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___7 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:174:6-174:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___8 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:186:6-186:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___9 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:222:6-222:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___10 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:234:6-234:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___11 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:265:6-265:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___12 == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:276:6-276:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond == 0' is always false (../plain/apache-get-tag.i.v+lhb-reducer.c:39:6-39:34)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:39:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:47:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:47:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:47:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:47:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:47:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:49:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:50:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:57:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:59:2)
[Success][Witness] invariant confirmed: (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:59:2)
[Success][Witness] invariant confirmed: 0 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:60:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:60:6)
[Success][Witness] invariant confirmed: (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:60:6)
[Success][Witness] invariant confirmed: 0 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:61:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Success][Witness] invariant confirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:63:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:67:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:67:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:67:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:67:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:79:2)
[Warning][Witness] invariant unconfirmed: -1LL + (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:90:3)
[Success][Witness] invariant confirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:90:3)
[Warning][Witness] invariant unconfirmed: -1LL + (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:91:2)
[Success][Witness] invariant confirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:91:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:100:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:101:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:104:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:105:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:109:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:109:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:109:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:111:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:112:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:121:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:123:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:124:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:131:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:131:6)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:131:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:132:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:132:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Warning][Witness] invariant unconfirmed: 2 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Warning][Witness] invariant unconfirmed: main__t != 1 (../plain/apache-get-tag.i.v+lhb-reducer.c:133:6)
[Warning][Witness] invariant unconfirmed: 2 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:137:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:137:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:137:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:137:2)
[Warning][Witness] invariant unconfirmed: main__t != 1 (../plain/apache-get-tag.i.v+lhb-reducer.c:137:2)
[Warning][Witness] invariant unconfirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: 2 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: main__t != 1 (../plain/apache-get-tag.i.v+lhb-reducer.c:149:2)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:171:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:171:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:171:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:173:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:174:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:183:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:185:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:186:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:193:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:193:6)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:193:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:194:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:194:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:215:6)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:219:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:219:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:219:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:221:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:222:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Warning][Witness] invariant unconfirmed: 1 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Warning][Witness] invariant unconfirmed: main__t != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:231:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:233:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:234:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:262:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:265:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:22:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:273:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:273:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:273:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:273:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:273:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:275:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:23:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:23:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:23:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:276:6)
[Success][Witness] invariant confirmed: 0 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:24:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:24:6)
[Success][Witness] invariant confirmed: (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:24:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:24:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:31:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:32:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:283:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:36:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: (long long )main__t >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.v+lhb-reducer.c:38:2)
[Success][Witness] invariant confirmed: 0 <= main__t (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.v+lhb-reducer.c:285:2)
[Info][Witness] witness validation summary:
  confirmed: 120
  unconfirmed: 46
  refuted: 0
  error: 34
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 200
SV-COMP result: unknown

vars = 193    evals = 268    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            3.510s     3.510s    483.96MB      1×
  preprocess                         0.026s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.63MB      4×
  Cabs2cil                           0.006s     0.006s      5.35MB      4×
  mergeCIL                           0.003s     0.003s      3.42MB      1×
  analysis                           3.465s     3.466s    465.36MB      1×
    createCFG                          0.001s     0.001s      0.94MB      1×
      handle                             0.001s     0.001s      0.20MB     33×
      iter_connect                       0.001s     0.001s      0.61MB     33×
        computeSCCs                        0.001s     0.001s      0.40MB     34×
    FrontC                             0.010s     0.010s      2.37MB    332×
    Cabs2cil                           0.077s     0.077s     31.33MB    332×
    global_inits                       0.001s     0.001s      0.49MB      1×
    solving                            2.853s     2.853s    234.91MB      1×
      S.Dom.equal                        0.001s     0.002s      0.10MB    270×
      base unassume                      0.131s     0.131s     80.65MB     14×
      cheap_full_reach                   0.001s     0.001s      0.07MB      1×
      postsolver                         0.543s     0.543s     47.30MB      1×
        postsolver_iter                    0.543s     0.543s     47.15MB      1×
    warn_global                        0.004s     0.004s      0.87MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
