/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.i.v+cfa-reducer.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/apache-escape-absolute.i.v+cfa-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/apache-escape-absolute.i.v+cfa-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: 1 <= main__c (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: main__c <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:279:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:281:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: 4 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:291:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:293:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:294:6)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:296:3)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:297:2)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:303:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:305:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:369:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:371:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6)
[Warning][Witness] couldn't locate invariant: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:381:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:383:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6)
[Warning][Witness] couldn't locate invariant: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: -1LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:421:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 0LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:426:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 0LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:431:2)
[Warning][Witness] couldn't locate invariant: 0 <= main__c (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 4 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__c <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:234:6)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: 4 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:238:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:240:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:241:6)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:243:3)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:244:2)
[Warning][Witness] couldn't locate invariant: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:250:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:252:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:261:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:262:6)
[Warning][Witness] couldn't locate invariant: 0 <= main__c (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: main__c <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:264:2)
[Warning][Witness] couldn't locate invariant: 1 <= main__c (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: 2 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: main__c <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: main__tokenlen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:267:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:269:2)
[Warning][Witness] couldn't locate invariant: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__c) + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Warning][Witness] couldn't locate invariant: ((1LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tokenlen != 0 && main__urilen != 1) && main__urilen != 0) && main__scheme != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && main__scheme <= 999999) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && 1 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL + (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && main__tokenlen <= 1000000) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && main__urilen <= 1000000) && -1000001LL + (long long )main__urilen >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__cp != 0) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__scheme != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__scheme <= 999999) && 1 <= main__scheme) && (long long )main__scheme - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__urilen != 0) && main__scheme != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen <= 1000000) && main__scheme <= 1000000) && 1 <= main__urilen) && 1 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000) && 0 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000) && -1000000 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__tokenlen <= 1000000) && -1000000 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && main__urilen <= 1000000) && -1000000 <= main__urilen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6-123:34)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tokenlen != 0 && main__urilen != 1) && main__urilen != 0) && main__scheme != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && main__scheme <= 999999) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && 1 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL + (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && main__tokenlen <= 1000000) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && main__urilen <= 1000000) && -1000001LL + (long long )main__urilen >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__cp != 0) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__cp >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__scheme != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__scheme <= 999999) && 1 <= main__scheme) && (long long )main__scheme - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__urilen != 0) && main__scheme != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen <= 1000000) && main__scheme <= 1000000) && 1 <= main__urilen) && 1 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000) && 0 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000) && -1000000 <= main__scheme) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && -1LL + (long long )main__urilen >= 0LL) && main__tokenlen <= 1000000) && -1000000 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL + (long long )main__scheme >= 0LL) && main__urilen <= 1000000) && -1000000 <= main__urilen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && -1000001LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && 1000000LL - (long long )main__scheme >= 0LL) && 1000000LL + (long long )main__tokenlen >= 0LL) && 1000000LL + (long long )main__urilen >= 0LL) && main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:391:2-391:25)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tokenlen != 0 && main__urilen != 1) && main__urilen != 0) && (long long )main__c >= 0LL) && ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -2LL + (long long )main__scheme >= 0LL) && main__c <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && main__scheme <= 999998) && 3 <= main__urilen) && 2 <= main__cp) && 2 <= main__scheme) && 1 <= main__tokenlen) && 0 <= main__c) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__c >= 0LL) && ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -2LL + (long long )main__scheme >= 0LL) && main__c <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1 <= main__tokenlen) && 0 <= main__c) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__scheme <= 999998) && 2 <= main__scheme) && (-1LL + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-3LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999998) && 1 <= main__cp) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6-224:34)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2-314:25)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__tokenlen != 0 && main__urilen != 1) && main__urilen != 0) && (long long )main__c >= 0LL) && ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -2LL + (long long )main__scheme >= 0LL) && main__c <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && main__scheme <= 999998) && 3 <= main__urilen) && 2 <= main__cp) && 2 <= main__scheme) && 1 <= main__tokenlen) && 0 <= main__c) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__c >= 0LL) && ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -2LL + (long long )main__scheme >= 0LL) && main__c <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1 <= main__tokenlen) && 0 <= main__c) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__cp <= 999998) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 3 <= main__urilen) && 2 <= main__cp) && 1 <= main__tokenlen) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -2LL + (long long )main__cp >= 0LL) && main__scheme <= 999998) && 2 <= main__scheme) && (-1LL + (long long )main__cp) - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999998) && 2 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-3LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999998) && 1 <= main__cp) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__tokenlen != 0) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__tokenlen <= 1000000) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && 1 <= main__tokenlen) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && main__urilen != 1) && main__urilen != 0) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL) && main__cp <= 999999) && main__urilen <= 1000000) && 2 <= main__urilen) && 1 <= main__cp) && (long long )main__cp - (long long )main__scheme >= 0LL) && 1000000LL - (long long )main__tokenlen >= 0LL) && 1000000LL - (long long )main__urilen >= 0LL) && (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL) && -1LL + (long long )main__tokenlen >= 0LL) && -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:314:2-314:25)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/apache-escape-absolute.i.v+cfa-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 85..86 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:85-86)
  on lines 97..98 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:97-98)
  on lines 113..114 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:113-114)
  on lines 125..126 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:125-126)
  on lines 145..146 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:145-146)
  on lines 157..158 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:157-158)
  on lines 177..178 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:177-178)
  on lines 189..190 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:189-190)
  on lines 214..215 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:214-215)
  on lines 226..227 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:226-227)
  on lines 255..256 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:255-256)
  on lines 272..273 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:272-273)
  on lines 284..285 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:284-285)
  on lines 308..309 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:308-309)
  on lines 374..375 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:374-375)
  on lines 386..387 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:386-387)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 108
  dead: 34 (2 in uncalled functions)
  total lines: 142
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___12 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:282:6-282:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6-83:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___14 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:306:6-306:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___0 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6-95:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___1 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6-111:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___15 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:372:6-372:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___2 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6-123:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___16 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:384:6-384:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___3 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6-143:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___4 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6-155:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___5 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6-175:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___6 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6-187:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___7 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6-212:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___8 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6-224:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___10 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:253:6-253:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___11 == 0' is always false (../plain/apache-escape-absolute.i.v+cfa-reducer.c:270:6-270:34)
[Success][Witness] invariant confirmed: main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:53:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:55:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:55:2)
[Error][Witness] invariant refuted: -1000001LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:55:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:55:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:55:2)
[Success][Witness] invariant confirmed: -1000000 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:59:6)
[Success][Witness] invariant confirmed: -1000000 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:61:6)
[Success][Witness] invariant confirmed: -1000000 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:63:6)
[Success][Witness] invariant confirmed: 0 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:65:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:67:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:67:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:67:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:67:2)
[Success][Witness] invariant confirmed: 1 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: 1 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: main__scheme <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: main__scheme != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:71:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:73:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:73:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:73:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:73:2)
[Error][Witness] invariant refuted: (long long )main__scheme - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:73:2)
[Success][Witness] invariant confirmed: 1 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: main__scheme <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: main__scheme != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:77:2)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:80:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:82:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:82:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:82:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:82:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:82:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:83:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:92:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:94:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:94:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:94:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:94:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:94:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:95:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:103:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:103:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:103:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:103:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:103:2)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:104:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:108:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:110:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:110:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:110:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:110:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:110:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:111:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:120:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:122:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:122:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:122:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:122:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:122:2)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: main__cp != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:123:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:134:2)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:135:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:140:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:142:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:143:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:152:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:154:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:155:6)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:162:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:165:3)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:165:3)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:165:3)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:165:3)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:165:3)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:166:2)
[Warning][Witness] invariant unconfirmed: (-1LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:166:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:166:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:166:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:166:2)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:172:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:174:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:175:6)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:184:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:186:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:187:6)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: 2 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Warning][Witness] invariant unconfirmed: main__cp <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:194:7)
[Success][Witness] invariant confirmed: 1 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Warning][Witness] invariant unconfirmed: (-3LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: (long long )main__cp - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:200:2)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:201:2)
[Success][Witness] invariant confirmed: 2 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: main__scheme <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:203:2)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: 3 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:204:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:206:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:206:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:206:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:206:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:206:2)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: 3 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:209:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:211:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:211:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:211:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:211:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:211:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:212:6)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:221:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:223:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:223:2)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:223:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:223:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:223:2)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Warning][Witness] invariant unconfirmed: main__cp <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__cp >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__cp) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:224:6)
[Success][Witness] invariant confirmed: 0 <= main__c (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: 2 <= main__cp (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: 3 <= main__urilen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__c <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Warning][Witness] invariant unconfirmed: (-2LL - (long long )main__scheme) + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: ((0LL - (long long )main__c) + (long long )main__cp) - (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: (long long )main__c >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__urilen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__urilen != 1 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Error][Witness] invariant refuted: -1000001LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:25:2)
[Success][Witness] invariant confirmed: main__urilen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:29:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:29:6)
[Error][Witness] invariant refuted: -1000001LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:31:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:35:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:35:6)
[Error][Witness] invariant refuted: -1000001LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:37:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:37:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:37:2)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:41:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:41:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:41:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:41:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:43:2)
[Error][Witness] invariant refuted: -1000001LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:43:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:43:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:47:6)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:47:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:47:6)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:47:6)
[Error][Witness] invariant refuted: -1000001LL + (long long )main__scheme >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:49:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:49:2)
[Success][Witness] invariant confirmed: 1000000LL + (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:49:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__urilen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:49:2)
[Success][Witness] invariant confirmed: 1000000LL - (long long )main__tokenlen >= 0LL (../plain/apache-escape-absolute.i.v+cfa-reducer.c:49:2)
[Success][Witness] invariant confirmed: 1 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: 1 <= main__tokenlen (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__scheme <= 999999 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__tokenlen <= 1000000 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__scheme != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: main__tokenlen != 0 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:131:6)
[Success][Witness] invariant confirmed: 2 <= main__scheme (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Success][Witness] invariant confirmed: main__scheme <= 999998 (../plain/apache-escape-absolute.i.v+cfa-reducer.c:232:6)
[Info][Witness] witness validation summary:
  confirmed: 440
  unconfirmed: 45
  refuted: 7
  error: 299
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 791
SV-COMP result: false

vars = 216    evals = 298    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            6.014s     6.015s   1727.74MB      1×
  preprocess                         0.024s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.70MB      4×
  Cabs2cil                           0.006s     0.006s      5.37MB      4×
  mergeCIL                           0.003s     0.003s      3.41MB      1×
  analysis                           5.973s     5.974s   1709.04MB      1×
    createCFG                          0.001s     0.001s      0.96MB      1×
      handle                             0.001s     0.001s      0.20MB     33×
      iter_connect                       0.001s     0.001s      0.62MB     33×
        computeSCCs                        0.001s     0.001s      0.41MB     34×
    FrontC                             0.021s     0.023s      7.66MB    984×
    Cabs2cil                           0.223s     0.224s     93.87MB    984×
    global_inits                       0.003s     0.003s      0.28MB      1×
    solving                            4.446s     4.446s    883.84MB      1×
      S.Dom.equal                        0.001s     0.002s      0.11MB    300×
      base unassume                      0.837s     0.837s    545.25MB     18×
      cheap_full_reach                   0.001s     0.001s      0.08MB      1×
      postsolver                         0.574s     0.574s     70.47MB      1×
        postsolver_iter                    0.574s     0.574s     70.31MB      1×
    warn_global                        0.001s     0.001s      0.90MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
