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


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


--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: 2 <= cp (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: 4 <= urilen (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: urilen <= 1000000 (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: (long long )c >= 0LL (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: urilen != 0 (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: urilen != 1 (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:67:17)
[Warning][Witness] couldn't locate invariant: 2 <= cp (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: (long long )c >= 0LL (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:68:17)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: (long long )c >= 0LL (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: 2 <= cp (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:69:21)
[Warning][Witness] couldn't locate invariant: 0 <= c (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: c <= 999998 (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: (long long )c >= 0LL (../plain/apache-escape-absolute.i:70:21)
[Warning][Witness] couldn't locate invariant: 1 <= c (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: 2 <= tokenlen (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: c <= 999999 (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )c >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: tokenlen != 0 (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: tokenlen != 1 (../plain/apache-escape-absolute.i:71:21)
[Warning][Witness] couldn't locate invariant: 1 <= c (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: c <= 999999 (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )c >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:72:21)
[Warning][Witness] couldn't locate invariant: 2 <= cp (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: 4 <= urilen (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: urilen <= 1000000 (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )c >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: urilen != 0 (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: urilen != 1 (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:73:21)
[Warning][Witness] couldn't locate invariant: 2 <= cp (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )c >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:74:21)
[Warning][Witness] couldn't locate invariant: 2 <= cp (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )c) + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: (long long )c >= 0LL (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: cp != 0 (../plain/apache-escape-absolute.i:76:17)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:82:5)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:82:5)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:82:5)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:82:5)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:82:5)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((tokenlen != 0 && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && -1000001LL - (long long )urilen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && urilen <= 1000000) && cp != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && 1 <= cp) && cp != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && cp != 0) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && 1 <= cp) && cp != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )scheme) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && scheme <= 999999) && 1 <= scheme) && tokenlen != 0) && urilen != 0) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && -1LL + (long long )scheme >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && 1 <= scheme) && tokenlen != 0) && urilen != 0) && (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && 0 <= scheme) && tokenlen != 0) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && -1000000 <= scheme) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= urilen) && -1000000 <= tokenlen) && -1000000 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && -1000000 <= tokenlen) && -1000000 <= urilen) && -1000000 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && -1000001LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && scheme <= 1000000) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && -1000001LL - (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:46:9-46:35)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((tokenlen != 0 && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && -1000001LL - (long long )urilen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && urilen <= 1000000) && cp != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && 1 <= cp) && cp != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && cp != 0) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && 1 <= cp) && cp != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )cp >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )scheme) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && scheme <= 999999) && 1 <= scheme) && tokenlen != 0) && urilen != 0) && scheme != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && -1LL + (long long )scheme >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && 1 <= scheme) && tokenlen != 0) && urilen != 0) && (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && 0 <= scheme) && tokenlen != 0) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= tokenlen) && 1 <= urilen) && -1000000 <= scheme) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && -1LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && 1 <= urilen) && -1000000 <= tokenlen) && -1000000 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL + (long long )scheme >= 0LL) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 1000000) && -1000000 <= tokenlen) && -1000000 <= urilen) && -1000000 <= scheme) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && -1000001LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL - (long long )scheme >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && scheme <= 1000000) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && -1000001LL - (long long )tokenlen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && tokenlen <= 1000000) && 1000000LL - (long long )urilen >= 0LL) && 1000000LL + (long long )urilen >= 0LL) && -1000001LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:51:13-51:17)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((tokenlen != 0 && urilen != 1) && urilen != 0) && (long long )c >= 0LL) && ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )scheme) + (long long )urilen >= 0LL) && -2LL + (long long )scheme >= 0LL) && c <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999998) && 3 <= urilen) && 2 <= cp) && 2 <= scheme) && 1 <= tokenlen) && 0 <= c) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && 2 <= cp) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && urilen <= 1000000) && 3 <= urilen) && 2 <= cp) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && tokenlen != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999998) && 3 <= urilen) && 2 <= cp) && 2 <= scheme) && 1 <= tokenlen) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && scheme <= 999998) && 2 <= scheme) && (-1LL + (long long )cp) - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999998) && 2 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-3LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999998) && 1 <= cp) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:64:13-64:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-escape-absolute.i:76:17-76:21)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((tokenlen != 0 && urilen != 1) && urilen != 0) && (long long )c >= 0LL) && ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )scheme) + (long long )urilen >= 0LL) && -2LL + (long long )scheme >= 0LL) && c <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999998) && 3 <= urilen) && 2 <= cp) && 2 <= scheme) && 1 <= tokenlen) && 0 <= c) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && 2 <= cp) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && urilen <= 1000000) && 3 <= urilen) && 2 <= cp) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && tokenlen != 0) && urilen != 1) && urilen != 0) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && cp <= 999998) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999998) && 3 <= urilen) && 2 <= cp) && 2 <= scheme) && 1 <= tokenlen) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -2LL + (long long )cp >= 0LL) && scheme <= 999998) && 2 <= scheme) && (-1LL + (long long )cp) - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999998) && 2 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-3LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999998) && 1 <= cp) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && tokenlen != 0) && urilen != 1) && urilen != 0) && scheme != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && tokenlen <= 1000000) && urilen <= 1000000) && scheme <= 999999) && 2 <= urilen) && 1 <= cp) && 1 <= tokenlen) && 1 <= scheme) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-1LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && urilen != 1) && urilen != 0) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL) && cp <= 999999) && urilen <= 1000000) && 2 <= urilen) && 1 <= cp) && (long long )cp - (long long )scheme >= 0LL) && 1000000LL - (long long )tokenlen >= 0LL) && 1000000LL - (long long )urilen >= 0LL) && (-2LL - (long long )cp) + (long long )urilen >= 0LL) && -1LL + (long long )tokenlen >= 0LL) && -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:76:17-76:21)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/apache-escape-absolute.i:14:1-16:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 51
  dead: 2 (2 in uncalled functions)
  total lines: 53
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/apache-escape-absolute.i:12:73-12:74)
[Error][Witness] invariant refuted: -1000001LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:32:53)
[Success][Witness] invariant confirmed: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:33:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:33:9)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:33:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:33:9)
[Success][Witness] invariant confirmed: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:33:57)
[Error][Witness] invariant refuted: -1000001LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:33:57)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:33:57)
[Error][Witness] invariant refuted: -1000001LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:33:57)
[Success][Witness] invariant confirmed: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: 1000000LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: scheme <= 1000000 (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:34:9)
[Success][Witness] invariant confirmed: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Success][Witness] invariant confirmed: 1000000LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Error][Witness] invariant refuted: -1000001LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Error][Witness] invariant refuted: -1000001LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:34:53)
[Success][Witness] invariant confirmed: -1000000 <= scheme (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: -1000000 <= urilen (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: -1000000 <= tokenlen (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: scheme <= 1000000 (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:35:8)
[Success][Witness] invariant confirmed: -1000000 <= scheme (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: -1000000 <= tokenlen (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1 <= urilen (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: scheme <= 1000000 (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: -1LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:36:8)
[Success][Witness] invariant confirmed: -1000000 <= scheme (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1 <= urilen (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: scheme <= 1000000 (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: -1LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1000000LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:37:8)
[Success][Witness] invariant confirmed: 0 <= scheme (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1 <= urilen (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: scheme <= 1000000 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: -1LL + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:38:9)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: scheme <= 999999 (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:41:5)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: -1LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: cp != 0 (../plain/apache-escape-absolute.i:42:5)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: -1LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: cp != 0 (../plain/apache-escape-absolute.i:43:5)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: -1LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: scheme <= 999999 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: cp != 0 (../plain/apache-escape-absolute.i:44:9)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: -1LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: cp != 0 (../plain/apache-escape-absolute.i:45:9)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: -1LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: cp != 0 (../plain/apache-escape-absolute.i:46:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:48:16)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:48:16)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:49:13)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:49:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:50:13)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:50:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:51:13)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:51:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:53:9)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:53:9)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:54:9)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:54:9)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: scheme <= 999999 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:55:13)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:55:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:56:9)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:56:9)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:57:9)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:57:9)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: scheme <= 999999 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:58:13)
[Warning][Witness] invariant unconfirmed: cp <= 999999 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:58:13)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:59:9)
[Warning][Witness] invariant unconfirmed: cp <= 999998 (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Warning][Witness] invariant unconfirmed: (-3LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:59:9)
[Success][Witness] invariant confirmed: 2 <= cp (../plain/apache-escape-absolute.i:60:9)
[Warning][Witness] invariant unconfirmed: cp <= 999998 (../plain/apache-escape-absolute.i:60:9)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:60:9)
[Success][Witness] invariant confirmed: 2 <= scheme (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: scheme <= 999998 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: -2LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:61:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: 2 <= cp (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: 3 <= urilen (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:61:13)
[Warning][Witness] invariant unconfirmed: cp <= 999998 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:61:13)
[Success][Witness] invariant confirmed: -2LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:62:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:62:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:62:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:62:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:62:13)
[Success][Witness] invariant confirmed: 2 <= cp (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: 3 <= urilen (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:63:13)
[Warning][Witness] invariant unconfirmed: cp <= 999998 (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: -2LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:63:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:63:13)
[Success][Witness] invariant confirmed: 2 <= cp (../plain/apache-escape-absolute.i:64:13)
[Warning][Witness] invariant unconfirmed: cp <= 999998 (../plain/apache-escape-absolute.i:64:13)
[Success][Witness] invariant confirmed: -2LL + (long long )cp >= 0LL (../plain/apache-escape-absolute.i:64:13)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:64:13)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:64:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:64:13)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:64:13)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:32:9)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:32:9)
[Error][Witness] invariant refuted: -1000001LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:32:53)
[Success][Witness] invariant confirmed: 1 <= scheme (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 1 <= cp (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 2 <= urilen (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: scheme <= 999999 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: cp <= 999999 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: -1LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: -1LL + (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: (-1LL - (long long )cp) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: (long long )cp - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: scheme != 0 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:47:17)
[Success][Witness] invariant confirmed: 0 <= c (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 1 <= tokenlen (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 2 <= scheme (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 2 <= cp (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 3 <= urilen (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: scheme <= 999998 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: urilen <= 1000000 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: tokenlen <= 1000000 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: c <= 999999 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: -2LL + (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )scheme) + (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 1000000LL - (long long )urilen >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: 1000000LL - (long long )tokenlen >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: ((0LL - (long long )c) + (long long )cp) - (long long )scheme >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: urilen != 0 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: urilen != 1 (../plain/apache-escape-absolute.i:65:21)
[Success][Witness] invariant confirmed: tokenlen != 0 (../plain/apache-escape-absolute.i:65:21)
[Info][Witness] witness validation summary:
  confirmed: 354
  unconfirmed: 35
  refuted: 6
  error: 107
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 502
SV-COMP result: false

vars = 159    evals = 372    narrow_reuses = 6

Timings:
                                  cputime   walltime   allocated   count
Default                            1.815s     1.815s   1216.34MB      1×
  preprocess                         0.031s     0.030s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.28MB      4×
  Cabs2cil                           0.005s     0.005s      4.95MB      4×
  mergeCIL                           0.003s     0.003s      3.37MB      1×
  analysis                           1.765s     1.766s   1198.67MB      1×
    createCFG                          0.001s     0.001s      0.76MB      1×
      handle                             0.001s     0.001s      0.14MB     34×
      iter_connect                       0.001s     0.001s      0.50MB     34×
        computeSCCs                        0.001s     0.001s      0.31MB     35×
    FrontC                             0.012s     0.012s      5.68MB    790×
    Cabs2cil                           0.129s     0.130s     73.69MB    790×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.264s     1.264s    659.26MB      1×
      S.Dom.equal                        0.001s     0.002s      0.13MB    378×
      base unassume                      0.660s     0.660s    444.84MB     26×
      cheap_full_reach                   0.001s     0.001s      0.06MB      1×
      postsolver                         0.062s     0.062s     38.11MB      1×
        postsolver_iter                    0.061s     0.061s     37.98MB      1×
    warn_global                        0.001s     0.001s      0.39MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
