/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-self2/ourtool.2023-02-15_09-12-33.files/ourtool/apache-get-tag.i.p+lhb-reducer.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/apache-get-tag.i.p+lhb-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/apache-get-tag.i.p+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: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:866:6)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:878:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:878:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:890:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:900:6)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:900:6)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:901:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:901:2)
[Warning][Witness] couldn't locate invariant: 10 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:902:2)
[Warning][Witness] couldn't locate invariant: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:902:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:914:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:914:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:926:2)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:936:6)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:936:6)
[Warning][Witness] couldn't locate invariant: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:937:2)
[Warning][Witness] couldn't locate invariant: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:937:2)
[Warning][Witness] couldn't locate invariant: 10 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:938:2)
[Warning][Witness] couldn't locate invariant: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:938:2)

runtime: 00:00:10.414
vars: 202, evals: 149

|rho|=202
|called|=9
|stable|=190
|infl|=190
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=146
Found 11 contexts for 2 functions. Top 5 functions:
10	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=605.19MB, max=31.05MB, minor=596.92MB, major=77.76MB, promoted=69.50MB
    minor collections=334  major collections=18 compactions=0


runtime: 00:00:20.431
vars: 209, evals: 163

|rho|=209
|called|=9
|stable|=209
|infl|=197
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=148
Found 12 contexts for 2 functions. Top 5 functions:
11	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=869.81MB, max=31.05MB, minor=861.53MB, major=115.25MB, promoted=106.97MB
    minor collections=535  major collections=26 compactions=0


runtime: 00:00:30.457
vars: 212, evals: 180

|rho|=212
|called|=9
|stable|=212
|infl|=200
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=150
Found 13 contexts for 2 functions. Top 5 functions:
12	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=1159.70MB, max=31.05MB, minor=1151.40MB, major=157.53MB, promoted=149.23MB
    minor collections=746  major collections=35 compactions=0


runtime: 00:00:40.481
vars: 215, evals: 197

|rho|=215
|called|=9
|stable|=215
|infl|=203
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=152
Found 14 contexts for 2 functions. Top 5 functions:
13	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=1452.45MB, max=31.05MB, minor=1444.13MB, major=199.74MB, promoted=191.42MB
    minor collections=955  major collections=42 compactions=0


runtime: 00:00:50.479
vars: 215, evals: 200

|rho|=215
|called|=9
|stable|=203
|infl|=203
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=152
Found 14 contexts for 2 functions. Top 5 functions:
13	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=1596.97MB, max=31.05MB, minor=1588.64MB, major=220.95MB, promoted=212.62MB
    minor collections=1102  major collections=48 compactions=0


runtime: 00:01:00.490
vars: 341, evals: 318

|rho|=341
|called|=15
|stable|=341
|infl|=320
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=258
Found 14 contexts for 2 functions. Top 5 functions:
13	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=1842.89MB, max=31.05MB, minor=1834.54MB, major=244.92MB, promoted=236.57MB
    minor collections=1280  major collections=56 compactions=0


runtime: 00:01:10.536
vars: 396, evals: 432

|rho|=396
|called|=22
|stable|=396
|infl|=381
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=299
Found 17 contexts for 2 functions. Top 5 functions:
16	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=2039.46MB, max=31.05MB, minor=2031.11MB, major=252.62MB, promoted=244.26MB
    minor collections=1413  major collections=64 compactions=0


runtime: 00:01:20.546
vars: 498, evals: 551

|rho|=500
|called|=0
|stable|=500
|infl|=492
|wpoint|=0
|side_dep|=35
|side_infl|=48
|var_messages|=0
|rho_write|=34
|dep|=390
Found 22 contexts for 3 functions. Top 5 functions:
16	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
5	contexts for entry state of reach_error (2000) on ../plain/apache-get-tag.i.p+lhb-reducer.c:4:1-4:96
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=2238.04MB, max=31.05MB, minor=2229.67MB, major=257.50MB, promoted=249.12MB
    minor collections=1540  major collections=71 compactions=0

[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__t != 1 && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 9 <= main__t) && 9 <= main__tagbuf_len) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= main__tagbuf_len) && -8LL + (long long )main__tagbuf_len >= 0LL) && 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__tagbuf_len) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= 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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__t != 1) && 2 <= main__t) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= 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) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (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__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= main__tagbuf_len) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= main__tagbuf_len) && 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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__t != 1) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 2 <= main__t) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && 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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= 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) && -7LL + (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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (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__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (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) && -6LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && 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) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 1 <= main__t) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (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) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 9 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (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) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (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) && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 9 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:862:2-862:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.p+lhb-reducer.c:937:2-937:23)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__t != 1 && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 9 <= main__t) && 9 <= main__tagbuf_len) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= main__tagbuf_len) && -8LL + (long long )main__tagbuf_len >= 0LL) && 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__tagbuf_len) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= 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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__t != 1) && 2 <= main__t) && main__t != 0) && 1 <= main__t) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -8LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 8 <= 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) && -8LL + (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) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (long long )main__tagbuf_len >= 0LL) && -8LL + (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__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= main__tagbuf_len) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= main__tagbuf_len) && 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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__t != 1) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 2 <= main__t) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && 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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -7LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 7 <= 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) && -7LL + (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) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (long long )main__tagbuf_len >= 0LL) && -7LL + (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__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && main__t != 0) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && 1 <= main__t) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (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) && -6LL + (long long )main__tagbuf_len >= 0LL) && (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && main__tagbuf_len <= 2147483646) && 1 <= main__tagbuf_len) && 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) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__t != 0) && main__t != -1) && main__t <= 2147483646) && 1 <= main__t) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (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) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 6 <= main__tagbuf_len) && (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && -6LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 5 <= main__tagbuf_len) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && -5LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 4 <= main__tagbuf_len) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && -4LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 3 <= main__tagbuf_len) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && -3LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -2LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 2 <= main__tagbuf_len) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 9 <= main__tagbuf_len) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -2LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (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) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (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) && main__tagbuf_len != 8) && main__tagbuf_len != 7) && main__tagbuf_len != 6) && main__tagbuf_len != 5) && main__tagbuf_len != 4) && main__tagbuf_len != 3) && main__tagbuf_len != 2) && main__tagbuf_len != 1) && main__tagbuf_len != 0) && main__tagbuf_len != -1) && -9LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 9 <= main__tagbuf_len) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:939:2-939:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:92:2-92:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:352:2-352:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:420:2-420:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:488:2-488:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:556:2-556:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:624:2-624:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:692:2-692:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:760:2-760:41)
[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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:828:2-828:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.p+lhb-reducer.c:901:2-901: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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:903:2-903:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.p+lhb-reducer.c:163:2-163:23)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-get-tag.i.p+lhb-reducer.c:225:2-225: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) && (0LL - (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) && -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__tagbuf_len >= 0LL) && -1LL + (long long )main__tagbuf_len >= 0LL) && main__tagbuf_len <= 2147483646) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && main__tagbuf_len <= 2147483646) && 0 <= main__t) && 0 <= main__tagbuf_len) && main__t <= 2147483646) && 0 <= main__t) && 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 (../plain/apache-get-tag.i.p+lhb-reducer.c:227:2-227:41)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/apache-get-tag.i.p+lhb-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 36..37 (../plain/apache-get-tag.i.p+lhb-reducer.c:36-37)
  on lines 48..49 (../plain/apache-get-tag.i.p+lhb-reducer.c:48-49)
  on line 74 (../plain/apache-get-tag.i.p+lhb-reducer.c:74-74)
  on line 85 (../plain/apache-get-tag.i.p+lhb-reducer.c:85-85)
  on lines 105..106 (../plain/apache-get-tag.i.p+lhb-reducer.c:105-106)
  on lines 117..118 (../plain/apache-get-tag.i.p+lhb-reducer.c:117-118)
  on lines 145..146 (../plain/apache-get-tag.i.p+lhb-reducer.c:145-146)
  on lines 173..174 (../plain/apache-get-tag.i.p+lhb-reducer.c:173-174)
  on lines 185..186 (../plain/apache-get-tag.i.p+lhb-reducer.c:185-186)
  on lines 207..208 (../plain/apache-get-tag.i.p+lhb-reducer.c:207-208)
  on lines 257..258 (../plain/apache-get-tag.i.p+lhb-reducer.c:257-258)
  on line 300 (../plain/apache-get-tag.i.p+lhb-reducer.c:300-300)
  on line 311 (../plain/apache-get-tag.i.p+lhb-reducer.c:311-311)
  on line 334 (../plain/apache-get-tag.i.p+lhb-reducer.c:334-334)
  on line 345 (../plain/apache-get-tag.i.p+lhb-reducer.c:345-345)
  on line 368 (../plain/apache-get-tag.i.p+lhb-reducer.c:368-368)
  on line 379 (../plain/apache-get-tag.i.p+lhb-reducer.c:379-379)
  on line 402 (../plain/apache-get-tag.i.p+lhb-reducer.c:402-402)
  on line 413 (../plain/apache-get-tag.i.p+lhb-reducer.c:413-413)
  on line 436 (../plain/apache-get-tag.i.p+lhb-reducer.c:436-436)
  on line 447 (../plain/apache-get-tag.i.p+lhb-reducer.c:447-447)
  on line 470 (../plain/apache-get-tag.i.p+lhb-reducer.c:470-470)
  on line 481 (../plain/apache-get-tag.i.p+lhb-reducer.c:481-481)
  on line 504 (../plain/apache-get-tag.i.p+lhb-reducer.c:504-504)
  on line 515 (../plain/apache-get-tag.i.p+lhb-reducer.c:515-515)
  on line 538 (../plain/apache-get-tag.i.p+lhb-reducer.c:538-538)
  on line 549 (../plain/apache-get-tag.i.p+lhb-reducer.c:549-549)
  on line 572 (../plain/apache-get-tag.i.p+lhb-reducer.c:572-572)
  on line 583 (../plain/apache-get-tag.i.p+lhb-reducer.c:583-583)
  on line 606 (../plain/apache-get-tag.i.p+lhb-reducer.c:606-606)
  on line 617 (../plain/apache-get-tag.i.p+lhb-reducer.c:617-617)
  on line 640 (../plain/apache-get-tag.i.p+lhb-reducer.c:640-640)
  on line 651 (../plain/apache-get-tag.i.p+lhb-reducer.c:651-651)
  on line 674 (../plain/apache-get-tag.i.p+lhb-reducer.c:674-674)
  on line 685 (../plain/apache-get-tag.i.p+lhb-reducer.c:685-685)
  on line 708 (../plain/apache-get-tag.i.p+lhb-reducer.c:708-708)
  on line 719 (../plain/apache-get-tag.i.p+lhb-reducer.c:719-719)
  on line 742 (../plain/apache-get-tag.i.p+lhb-reducer.c:742-742)
  on line 753 (../plain/apache-get-tag.i.p+lhb-reducer.c:753-753)
  on line 776 (../plain/apache-get-tag.i.p+lhb-reducer.c:776-776)
  on line 787 (../plain/apache-get-tag.i.p+lhb-reducer.c:787-787)
  on line 810 (../plain/apache-get-tag.i.p+lhb-reducer.c:810-810)
  on line 821 (../plain/apache-get-tag.i.p+lhb-reducer.c:821-821)
  on line 844 (../plain/apache-get-tag.i.p+lhb-reducer.c:844-844)
  on line 855 (../plain/apache-get-tag.i.p+lhb-reducer.c:855-855)
  on lines 883..884 (../plain/apache-get-tag.i.p+lhb-reducer.c:883-884)
  on lines 919..920 (../plain/apache-get-tag.i.p+lhb-reducer.c:919-920)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 287
  dead: 60 (2 in uncalled functions)
  total lines: 347
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___0 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:46:6-46:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___14 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:309:6-309:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___44 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:819:6-819:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___29 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:570:6-570:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___30 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:581:6-581:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___1 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:72:6-72:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___45 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:842:6-842:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___15 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:332:6-332:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___2 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:83:6-83:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___46 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:853:6-853:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___16 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:343:6-343:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___31 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:604:6-604:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___32 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:615:6-615:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___3 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:103:6-103:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___17 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:366:6-366:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___18 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:377:6-377:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___47 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:881:6-881:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___4 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:115:6-115:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___33 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:638:6-638:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___34 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:649:6-649:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___19 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:400:6-400:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___5 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:143:6-143:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___20 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:411:6-411:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___49 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:917:6-917:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___35 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:672:6-672:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___36 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:683:6-683:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___21 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:434:6-434:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___7 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:171:6-171:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___22 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:445:6-445:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___37 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:706:6-706:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___8 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6-183:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___38 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:717:6-717:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___23 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:468:6-468:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___9 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:205:6-205:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___24 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:479:6-479:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___39 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:740:6-740:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___40 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:751:6-751:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___25 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:502:6-502:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___26 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:513:6-513:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___41 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:774:6-774:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___11 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:255:6-255:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___42 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:785:6-785:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___27 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:536:6-536:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:34:6-34:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___28 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:547:6-547:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___13 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:298:6-298:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___43 == 0' is always false (../plain/apache-get-tag.i.p+lhb-reducer.c:808:6-808:34)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:805:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:295:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:807:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:297:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:808:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:298:6)
[Success][Witness] invariant confirmed: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:816:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:306:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:818:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:308:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:309:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:819:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:315:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:825:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:316:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:826:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:317:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:317:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:317:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:317:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:317:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:827:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:828:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:324:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:839:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:325:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:841:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:842:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:329:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:331:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:332:6)
[Success][Witness] invariant confirmed: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:850:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:852:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:853:6)

runtime: 00:01:30.660
vars: 498, evals: 551

|rho|=488
|called|=0
|stable|=488
|infl|=480
|wpoint|=0
|side_dep|=104
|side_infl|=212
|var_messages|=17
|rho_write|=159
|dep|=382
Found 18 contexts for 3 functions. Top 5 functions:
12	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
5	contexts for entry state of reach_error (2000) on ../plain/apache-get-tag.i.p+lhb-reducer.c:4:1-4:96
1	contexts for entry state of main (2011) on ../plain/apache-get-tag.i.p+lhb-reducer.c:17:2-1006:2

Memory statistics: total=2690.23MB, max=31.05MB, minor=2680.26MB, major=271.42MB, promoted=261.46MB
    minor collections=1776  major collections=81 compactions=0

[Success][Witness] invariant confirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:340:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:342:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:343:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:859:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:860:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:349:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:861:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:350:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:862:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:351:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:352:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:363:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:365:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:366:6)
[Success][Witness] invariant confirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:374:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:376:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:377:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:383:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:384:2)
[Success][Witness] invariant confirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:385:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:392:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:393:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:397:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:399:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:400:6)
[Success][Witness] invariant confirmed: 3 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:408:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:410:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:411:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:417:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:418:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:419:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:420:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:431:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:433:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:434:6)
[Success][Witness] invariant confirmed: 3 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:442:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:444:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:445:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:451:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:452:2)
[Success][Witness] invariant confirmed: 3 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:453:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:460:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:461:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:465:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:467:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:468:6)
[Success][Witness] invariant confirmed: 4 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:476:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:478:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:479:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:485:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:486:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:487:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:488:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:499:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:501:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:502:6)
[Success][Witness] invariant confirmed: 4 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:510:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:512:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:513:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:519:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:520:2)
[Success][Witness] invariant confirmed: 4 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:521:6)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:528:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:24:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:529:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:25:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:25:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:25:2)
[Success][Witness] invariant confirmed: 0 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:26:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:26:6)
[Success][Witness] invariant confirmed: (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:26:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:26:6)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:533:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:535:2)
[Success][Witness] invariant confirmed: 0 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:31:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:31:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:536:6)
[Success][Witness] invariant confirmed: 5 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:544:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:546:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:547:6)
[Success][Witness] invariant confirmed: 0 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:43:2)
[Success][Witness] invariant confirmed: 0 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:43:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:43:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:43:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:553:6)
[Success][Witness] invariant confirmed: 0 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:46:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:46:6)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:554:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:555:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:556:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:567:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:569:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:570:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:64:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:65:6)
[Success][Witness] invariant confirmed: 5 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:578:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:580:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:69:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:581:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:71:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:72:6)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:587:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:80:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:80:2)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:588:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:82:2)
[Success][Witness] invariant confirmed: 5 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: -5LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:589:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:83:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:596:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:89:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:597:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:90:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:91:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:601:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:92:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:603:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:604:6)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:95:2)
[Success][Witness] invariant confirmed: 6 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:612:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:96:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:614:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:615:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:100:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:100:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:100:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:100:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:621:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:622:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:623:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:624:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:112:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:115:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:115:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:115:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:115:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:635:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:637:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:638:6)
[Success][Witness] invariant confirmed: 6 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:646:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:648:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:131:2)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:649:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:132:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:135:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:136:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:655:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:656:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:140:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:140:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:140:2)
[Success][Witness] invariant confirmed: 6 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: -6LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:657:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:142:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:143:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:664:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:665:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:669:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:671:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:152:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:672:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:154:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:155:6)
[Success][Witness] invariant confirmed: 7 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:680:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:682:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:683:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:162:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:162:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:163:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: 2 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:164:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:689:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:690:2)
[Success][Witness] invariant confirmed: 2 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:168:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:168:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:168:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:168:2)
[Success][Witness] invariant confirmed: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:168:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:691:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:692:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:703:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:705:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:706:6)
[Success][Witness] invariant confirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: 2 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Warning][Witness] invariant unconfirmed: main__t <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__t != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:180:2)
[Success][Witness] invariant confirmed: 7 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:714:2)
[Success][Witness] invariant confirmed: 2 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:183:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:716:2)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:717:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:723:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:724:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:202:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:202:2)
[Success][Witness] invariant confirmed: 7 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: -7LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:725:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:204:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:205:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:732:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:733:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:737:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:739:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:214:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:740:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:216:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:217:6)
[Success][Witness] invariant confirmed: 8 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:748:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:750:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:751:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:224:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:224:6)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:224:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:225:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:225:2)
[Success][Witness] invariant confirmed: 2 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:226:2)
[Success][Witness] invariant confirmed: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:226:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:757:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:758:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:759:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:760:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:247:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:771:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:248:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:773:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:774:6)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:252:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:252:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:252:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:254:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:255:6)
[Success][Witness] invariant confirmed: 8 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:782:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:784:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:785:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Success][Witness] invariant confirmed: main__t != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:264:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:266:2)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:791:6)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:267:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:267:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__t) + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:267:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:267:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:267:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:792:2)
[Success][Witness] invariant confirmed: 8 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: -8LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:793:6)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:800:2)
[Success][Witness] invariant confirmed: -9LL + (long long )main__tagbuf_len >= 0LL (../plain/apache-get-tag.i.p+lhb-reducer.c:801:6)
[Success][Witness] invariant confirmed: 9 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: 9 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 2 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 3 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 4 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 5 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 6 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 7 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 8 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: main__t != 1 (../plain/apache-get-tag.i.p+lhb-reducer.c:864:2)
[Success][Witness] invariant confirmed: 1 <= main__tagbuf_len (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Success][Witness] invariant confirmed: 1 <= main__t (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Success][Witness] invariant confirmed: main__tagbuf_len <= 2147483646 (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != -1 (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Success][Witness] invariant confirmed: main__tagbuf_len != 0 (../plain/apache-get-tag.i.p+lhb-reducer.c:94:2)
[Info][Witness] witness validation summary:
  confirmed: 520
  unconfirmed: 36
  refuted: 0
  error: 57
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 613
SV-COMP result: unknown

vars = 498    evals = 551    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                           95.779s    95.789s   2850.63MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.57MB      4×
  Cabs2cil                           0.006s     0.006s      6.54MB      4×
  mergeCIL                           0.004s     0.004s      3.56MB      1×
  analysis                          95.735s    95.744s   2829.33MB      1×
    createCFG                          0.005s     0.005s      1.60MB      1×
      handle                             0.001s     0.001s      0.40MB     33×
      iter_connect                       0.005s     0.005s      1.02MB     33×
        computeSCCs                        0.004s     0.004s      0.75MB     34×
    FrontC                             0.020s     0.022s      7.54MB   1112×
    Cabs2cil                           0.523s     0.524s    107.84MB   1112×
    global_inits                       0.001s     0.001s      0.70MB      1×
    solving                           89.697s    89.706s   2088.25MB      1×
      S.Dom.equal                        0.002s     0.004s      0.19MB    553×
      base unassume                      2.251s     2.252s   1013.77MB     52×
      cheap_full_reach                   0.001s     0.001s      0.19MB      1×
      postsolver                        12.444s    12.446s    273.52MB      1×
        postsolver_iter                   12.444s    12.445s    273.14MB      1×
    warn_global                        0.002s     0.002s      2.11MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
