Add some regressions. Minor.

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ac23dae29515ef8c3db220fb5fd405fdfb4bc280..259083e6eb33828a4a1cd62592913a27eea092a4 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -681,7 +681,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
                 cond.insert( cond.end(), inst.begin(), inst.end() );
                 //need to do exhaustive instantiate algorithm to set things properly (should only add one instance)
                 Node c = mkCond( cond );
-                int prevInst = d_addedLemmas;
+                unsigned prevInst = d_addedLemmas;
                 exhaustiveInstantiate( fmfmc, f, c, -1 );
                 if( d_addedLemmas==prevInst ){
                   d_star_insts[f].push_back(i);

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index dc87e107736915eb469d8330076aa49737a465a6..0f41c22ec890d3af3d69b504a12bdf9a9dc97335 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -98,6 +98,7 @@ SMT_TESTS = \
        bv2nat-ground-c.smt2 \
        cmu-rdk-3.smt2 \
        bv2nat-simp-range.smt2 \
+       bv2nat-simp-range-sat.smt2 \
        bv-int-collapse1.smt2 \
        bv-int-collapse2.smt2 \
        bv-int-collapse2-sat.smt2

diff --git a/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2
new file mode 100644 (file)
index 0000000..7e98460
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun t () (_ BitVec 16))
+(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65535))))
+(check-sat)

diff --git a/test/regress/regress1/fmf/Makefile.am b/test/regress/regress1/fmf/Makefile.am
index 3cb00d6ae8885b6659e0ce8d6af169160ee55e4b..efaf535c6d5f0fdce96f2ce08239c507a116eecf 100644 (file)
--- a/test/regress/regress1/fmf/Makefile.am
+++ b/test/regress/regress1/fmf/Makefile.am
@@ -17,7 +17,8 @@ endif
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =        \
-       ForElimination-scala-9.smt2
+       ForElimination-scala-9.smt2 \
+       nunchaku2309663.nun.min.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2 b/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
new file mode 100644 (file)
index 0000000..076150d
--- /dev/null
+++ b/test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2
@@ -0,0 +1,79 @@
+; EXPECT: unsat
+; COMMAND-LINE: --finite-model-find
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((nat__ (Suc__ (_select_Suc___0 nat__)) (zero__ ))))
+(declare-sort a__ 0)
+(declare-fun __nun_card_witness_0_ () a__)
+(declare-datatypes ()
+   ((tree__
+       (MKT__ (_select_MKT___0 a__) (_select_MKT___1 tree__) 
+          (_select_MKT___2 tree__) (_select_MKT___3 nat__)) 
+       (ET__ ))))
+(declare-sort G_plus__ 0)
+(declare-fun __nun_card_witness_1_ () G_plus__)
+(declare-fun plus__ (nat__ nat__) nat__)
+(declare-fun proj_G_plus__0_ (G_plus__) nat__)
+(declare-fun proj_G_plus__1_ (G_plus__) nat__)
+
+(declare-sort G_less__eq__ 0)
+(declare-fun __nun_card_witness_2_ () G_less__eq__)
+(declare-fun less__eq__ (nat__ nat__) Bool)
+(declare-fun proj_G_less__eq__0_ (G_less__eq__) nat__)
+(declare-fun proj_G_less__eq__1_ (G_less__eq__) nat__)
+
+(declare-sort G_max__ 0)
+(declare-fun __nun_card_witness_3_ () G_max__)
+(declare-fun max__ (nat__ nat__) nat__)
+(declare-fun proj_G_max__0_ (G_max__) nat__)
+(declare-fun proj_G_max__1_ (G_max__) nat__)
+
+(declare-sort G_one__ 0)
+(declare-fun __nun_card_witness_4_ () G_one__)
+(declare-fun one__ () nat__)
+(assert (forall ((a/295 G_one__)) (= one__ (Suc__ zero__))))
+(declare-sort G_height__ 0)
+(declare-fun __nun_card_witness_5_ () G_height__)
+(declare-fun height__ (tree__) nat__)
+(declare-fun proj_G_height__0_ (G_height__) tree__)
+
+(declare-sort G_avl__ 0)
+(declare-fun __nun_card_witness_6_ () G_avl__)
+(declare-fun avl__ (tree__) Bool)
+(declare-fun proj_G_avl__0_ (G_avl__) tree__)
+
+(declare-fun l__ () tree__)
+(declare-fun r__ () tree__)
+(declare-sort G_minus__ 0)
+(declare-fun __nun_card_witness_7_ () G_minus__)
+(declare-fun minus__ (Bool Bool) Bool)
+(declare-fun proj_G_minus__0_ (G_minus__) Bool)
+(declare-fun proj_G_minus__1_ (G_minus__) Bool)
+
+(declare-sort G_ht__ 0)
+(declare-fun __nun_card_witness_8_ () G_ht__)
+(declare-fun ht__ (tree__) nat__)
+(declare-fun proj_G_ht__0_ (G_ht__) tree__)
+
+(declare-sort G_mkt__ 0)
+(declare-fun __nun_card_witness_9_ () G_mkt__)
+(declare-fun mkt__ (a__ tree__ tree__) tree__)
+(declare-fun proj_G_mkt__0_ (G_mkt__) a__)
+(declare-fun proj_G_mkt__1_ (G_mkt__) tree__)
+(declare-fun proj_G_mkt__2_ (G_mkt__) tree__)
+
+(declare-fun x__ () a__)
+
+(assert (and
+(forall ((a/334 G_avl__)) (and (= (avl__ (proj_G_avl__0_ a/334)) (=> (is-MKT__ (proj_G_avl__0_ a/334)) (and (or (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (plus__ (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) one__)) (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (plus__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) one__))) (= (_select_MKT___3 (proj_G_avl__0_ a/334)) (plus__ (max__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) one__)) (avl__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (avl__ (_select_MKT___2 (proj_G_avl__0_ a/334)))))) (exists ((a/602 G_avl__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_avl__0_ a/602)) ) (exists ((a/601 G_avl__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_avl__0_ a/601)) ) (exists ((a/592 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_max__1_ a/592)) (exists ((a/595 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/595)) ) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_max__0_ a/592)) (exists ((a/596 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/596)) )) ) (exists ((a/600 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/600)) ) (exists ((a/599 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/599)) ) (exists ((a/564 G_plus__)) (and (= one__ (proj_G_plus__1_ a/564)) (= (max__ (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (height__ (_select_MKT___2 (proj_G_avl__0_ a/334)))) (proj_G_plus__0_ a/564)) (exists ((a/581 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/581)) ) (exists ((a/582 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/582)) ) (exists ((a/574 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_max__1_ a/574)) (exists ((a/577 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/577)) ) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_max__0_ a/574)) (exists ((a/578 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/578)) )) )) ) (exists ((a/551 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/551)) ) (exists ((a/550 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/550)) ) (exists ((a/557 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/557)) ) (exists ((a/552 G_plus__)) (and (= one__ (proj_G_plus__1_ a/552)) (= (height__ (_select_MKT___2 (proj_G_avl__0_ a/334))) (proj_G_plus__0_ a/552)) (exists ((a/554 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/554)) )) ) (exists ((a/556 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/556)) ) (exists ((a/563 G_height__)) (= (_select_MKT___2 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/563)) ) (exists ((a/558 G_plus__)) (and (= one__ (proj_G_plus__1_ a/558)) (= (height__ (_select_MKT___1 (proj_G_avl__0_ a/334))) (proj_G_plus__0_ a/558)) (exists ((a/560 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/560)) )) ) (exists ((a/562 G_height__)) (= (_select_MKT___1 (proj_G_avl__0_ a/334)) (proj_G_height__0_ a/562)) )) )
+(forall ((a/603 G_minus__)) (= (minus__ (proj_G_minus__0_ a/603) (proj_G_minus__1_ a/603)) (ite (proj_G_minus__0_ a/603) (ite (proj_G_minus__1_ a/603) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603))) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603)))) (ite (proj_G_minus__1_ a/603) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603))) (and (proj_G_minus__0_ a/603) (not (proj_G_minus__1_ a/603)))))) )
+(forall ((a/296 G_height__)) (and (= (height__ (proj_G_height__0_ a/296)) (ite (is-MKT__ (proj_G_height__0_ a/296)) (plus__ (max__ (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (height__ (_select_MKT___2 (proj_G_height__0_ a/296)))) one__) zero__)) (=> (is-MKT__ (proj_G_height__0_ a/296)) (and (exists ((a/297 G_plus__)) (and (= one__ (proj_G_plus__1_ a/297)) (= (max__ (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (height__ (_select_MKT___2 (proj_G_height__0_ a/296)))) (proj_G_plus__0_ a/297)) (exists ((a/314 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/314)) ) (exists ((a/315 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/315)) ) (exists ((a/307 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_height__0_ a/296))) (proj_G_max__1_ a/307)) (exists ((a/310 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/310)) ) (= (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (proj_G_max__0_ a/307)) (exists ((a/311 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/311)) )) )) ) (exists ((a/332 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/332)) ) (exists ((a/333 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/333)) ) (exists ((a/325 G_max__)) (and (= (height__ (_select_MKT___2 (proj_G_height__0_ a/296))) (proj_G_max__1_ a/325)) (exists ((a/328 G_height__)) (= (_select_MKT___2 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/328)) ) (= (height__ (_select_MKT___1 (proj_G_height__0_ a/296))) (proj_G_max__0_ a/325)) (exists ((a/329 G_height__)) (= (_select_MKT___1 (proj_G_height__0_ a/296)) (proj_G_height__0_ a/329)) )) )))) )
+(forall ((a/604 G_ht__)) (= (ht__ (proj_G_ht__0_ a/604)) (ite (is-MKT__ (proj_G_ht__0_ a/604)) (_select_MKT___3 (proj_G_ht__0_ a/604)) zero__)) )
+
+(not (=> (and (avl__ l__) (exists ((a/1961 G_avl__)) (= l__ (proj_G_avl__0_ a/1961)) )) (=> (and (avl__ r__) (exists ((a/2175 G_avl__)) (= r__ (proj_G_avl__0_ a/2175)) )) (=> (or (and (= (height__ l__) (height__ r__)) (exists ((a/2334 G_height__)) (= l__ (proj_G_height__0_ a/2334)) ) (exists ((a/2333 G_height__)) (= r__ (proj_G_height__0_ a/2333)) )) (and (minus__ (= (height__ l__) (plus__ (height__ r__) one__)) (= (height__ r__) (plus__ (height__ l__) one__))) (exists ((a/2382 G_height__)) (= l__ (proj_G_height__0_ a/2382)) ) (exists ((a/2378 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2378)) (= (height__ l__) (proj_G_plus__0_ a/2378)) (exists ((a/2380 G_height__)) (= l__ (proj_G_height__0_ a/2380)) )) ) (exists ((a/2383 G_height__)) (= r__ (proj_G_height__0_ a/2383)) ) (exists ((a/2376 G_height__)) (= r__ (proj_G_height__0_ a/2376)) ) (exists ((a/2372 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2372)) (= (height__ r__) (proj_G_plus__0_ a/2372)) (exists ((a/2374 G_height__)) (= r__ (proj_G_height__0_ a/2374)) )) ) (exists ((a/2377 G_height__)) (= l__ (proj_G_height__0_ a/2377)) ) (exists ((a/2335 G_minus__)) (and (= (= (height__ r__) (plus__ (height__ l__) one__)) (proj_G_minus__1_ a/2335)) (exists ((a/2352 G_height__)) (= l__ (proj_G_height__0_ a/2352)) ) (exists ((a/2348 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2348)) (= (height__ l__) (proj_G_plus__0_ a/2348)) (exists ((a/2350 G_height__)) (= l__ (proj_G_height__0_ a/2350)) )) ) (exists ((a/2353 G_height__)) (= r__ (proj_G_height__0_ a/2353)) ) (= (= (height__ l__) (plus__ (height__ r__) one__)) (proj_G_minus__0_ a/2335)) (exists ((a/2358 G_height__)) (= r__ (proj_G_height__0_ a/2358)) ) (exists ((a/2354 G_plus__)) (and (= one__ (proj_G_plus__1_ a/2354)) (= (height__ r__) (proj_G_plus__0_ a/2354)) (exists ((a/2356 G_height__)) (= r__ (proj_G_height__0_ a/2356)) )) ) (exists ((a/2359 G_height__)) (= l__ (proj_G_height__0_ a/2359)) )) ))) (=> (exists ((a/2384 G_avl__)) (and (= (mkt__ x__ l__ r__) (proj_G_avl__0_ a/2384)) (exists ((a/2385 G_mkt__)) (and (= r__ (proj_G_mkt__2_ a/2385)) (= l__ (proj_G_mkt__1_ a/2385)) (= x__ (proj_G_mkt__0_ a/2385))) )) ) (=> (exists ((a/2387 G_mkt__)) (and (= r__ (proj_G_mkt__2_ a/2387)) (= l__ (proj_G_mkt__1_ a/2387)) (= x__ (proj_G_mkt__0_ a/2387))) ) (avl__ (mkt__ x__ l__ r__))))))))
+(forall ((a/605 G_mkt__)) (and (= (mkt__ (proj_G_mkt__0_ a/605) (proj_G_mkt__1_ a/605) (proj_G_mkt__2_ a/605)) (MKT__ (proj_G_mkt__0_ a/605) (proj_G_mkt__1_ a/605) (proj_G_mkt__2_ a/605) (plus__ (max__ (ht__ (proj_G_mkt__1_ a/605)) (ht__ (proj_G_mkt__2_ a/605))) one__))) (exists ((a/671 G_max__)) (and (= (ht__ (proj_G_mkt__2_ a/605)) (proj_G_max__1_ a/671)) (exists ((a/674 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/674)) ) (= (ht__ (proj_G_mkt__1_ a/605)) (proj_G_max__0_ a/671)) (exists ((a/675 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/675)) )) ) (exists ((a/679 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/679)) ) (exists ((a/678 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/678)) ) (exists ((a/643 G_plus__)) (and (= one__ (proj_G_plus__1_ a/643)) (= (max__ (ht__ (proj_G_mkt__1_ a/605)) (ht__ (proj_G_mkt__2_ a/605))) (proj_G_plus__0_ a/643)) (exists ((a/660 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/660)) ) (exists ((a/661 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/661)) ) (exists ((a/653 G_max__)) (and (= (ht__ (proj_G_mkt__2_ a/605)) (proj_G_max__1_ a/653)) (exists ((a/656 G_ht__)) (= (proj_G_mkt__2_ a/605) (proj_G_ht__0_ a/656)) ) (= (ht__ (proj_G_mkt__1_ a/605)) (proj_G_max__0_ a/653)) (exists ((a/657 G_ht__)) (= (proj_G_mkt__1_ a/605) (proj_G_ht__0_ a/657)) )) )) )) )
+(forall ((a/295 G_one__)) (= one__ (Suc__ zero__)) )
+
+))
+  
+(check-sat)

diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
index 7830f14f15845db195be106e73f306cecf5ca6a4..716e664b1fc95681db51ecb158ca515acd611e6e 100644 (file)
--- a/test/regress/regress1/strings/Makefile.am
+++ b/test/regress/regress1/strings/Makefile.am
@@ -18,7 +18,9 @@ endif
 # put it below in "TESTS +="
 TESTS =        \
        cmu-5042-0707-2.smt2 \
-       cmu-dis-0707-3.smt2
+       cmu-dis-0707-3.smt2 \
+       cmu-prereg-fmf.smt2 \
+       cmu-repl-len-nterm.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/strings/cmu-prereg-fmf.smt2 b/test/regress/regress1/strings/cmu-prereg-fmf.smt2
new file mode 100644 (file)
index 0000000..0d6827c
--- /dev/null
+++ b/test/regress/regress1/strings/cmu-prereg-fmf.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun url () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "Y") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "X") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "W") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "V") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "U") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "T") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "S") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "R") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "Q") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "P") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "O") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "N") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "M") 1 0) 0)))) (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) "K" "k") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) "K" "k") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))))) "L") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1))) "K") 1 0) 0)))) (not (= (ite (str.contains (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K") 1 0) 0))) (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K") 1 0) 0))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "J") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "I") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "H") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "G") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "F") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "E") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "D") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "C") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "A") 1 0) 0)))) (not (not (= (ite (not (= (str.len (str.substr url (+ (str.indexof url ":" 0) 1) (- (str.len url) (+ (str.indexof url ":" 0) 1)))) 0)) 1 0) 0)))) (not (not (= (ite (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http") 1 0) 0)))) (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (not (= (ite (not (= (str.len url) 0)) 1 0) 0))) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1))) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "K" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof url ":" 0) 1) 0)) (>= (- (str.len url) (+ (str.indexof url ":" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)))
+
+(check-sat)
+
+;(get-value (url))

diff --git a/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2
new file mode 100644 (file)
index 0000000..004db77
--- /dev/null
+++ b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun url () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) "B" "b") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) "B" "b") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))))) "C") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))) "B") 1 0) 0)))) (not (= (ite (str.contains (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B") 1 0) 0))) (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B") 1 0) 0))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "A") 1 0) 0)))) (not (not (= (ite (not (= (str.len (str.substr url (+ (str.indexof url ":" 0) 1) (- (str.len url) (+ (str.indexof url ":" 0) 1)))) 0)) 1 0) 0)))) (not (not (= (ite (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http") 1 0) 0)))) (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof url ":" 0) 1) 0)) (>= (- (str.len url) (+ (str.indexof url ":" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)))
+
+(check-sat)
+
+;(get-value (url))

diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
index 0451f93da51865064a6502e8c562c15d3bd16c9d..2dff1f1daa003660530cca6ea20f9e8ee34a64f9 100644 (file)
--- a/test/regress/regress1/sygus/Makefile.am
+++ b/test/regress/regress1/sygus/Makefile.am
@@ -17,7 +17,8 @@ endif
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =        \
-       hd-sdiv.sy
+       hd-sdiv.sy \
+       stopwatch-bt.sy
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
new file mode 100644 (file)
index 0000000..0162805
--- /dev/null
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -0,0 +1,230 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+(set-logic LIA)
+
+(define-fun
+  __node_init_previous_0 (
+    (previous.usr.x@0 Int)
+    (previous.usr.y@0 Int)
+    (previous.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= previous.usr.y@0 0) previous.res.init_flag@0)
+)
+
+(define-fun
+  __node_trans_previous_0 (
+    (previous.usr.x@1 Int)
+    (previous.usr.y@1 Int)
+    (previous.res.init_flag@1 Bool)
+    (previous.usr.x@0 Int)
+    (previous.usr.y@0 Int)
+    (previous.res.init_flag@0 Bool)
+  ) Bool
+  
+  (and (= previous.usr.y@1 previous.usr.x@0) (not previous.res.init_flag@1))
+)
+
+(define-fun
+  __node_init_stopwatch_0 (
+    (stopwatch.usr.toggle@0 Bool)
+    (stopwatch.usr.reset@0 Bool)
+    (stopwatch.usr.count@0 Int)
+    (stopwatch.res.init_flag@0 Bool)
+    (stopwatch.res.abs_0@0 Bool)
+    (stopwatch.impl.usr.running@0 Bool)
+    (stopwatch.res.abs_1@0 Int)
+    (stopwatch.res.inst_0@0 Bool)
+  ) Bool
+  
+  (and
+   (= stopwatch.impl.usr.running@0 (not (not stopwatch.usr.toggle@0)))
+   (=
+    stopwatch.usr.count@0
+    (ite
+     stopwatch.usr.reset@0
+     0
+     (ite
+      stopwatch.impl.usr.running@0
+      (+ stopwatch.res.abs_1@0 1)
+      stopwatch.res.abs_1@0)))
+   (= stopwatch.res.abs_0@0 (>= stopwatch.usr.count@0 0))
+   (__node_init_previous_0
+    stopwatch.usr.count@0
+    stopwatch.res.abs_1@0
+    stopwatch.res.inst_0@0)
+   stopwatch.res.init_flag@0
+   true)
+)
+
+(define-fun
+  __node_trans_stopwatch_0 (
+    (stopwatch.usr.toggle@1 Bool)
+    (stopwatch.usr.reset@1 Bool)
+    (stopwatch.usr.count@1 Int)
+    (stopwatch.res.init_flag@1 Bool)
+    (stopwatch.res.abs_0@1 Bool)
+    (stopwatch.impl.usr.running@1 Bool)
+    (stopwatch.res.abs_1@1 Int)
+    (stopwatch.res.inst_0@1 Bool)
+    (stopwatch.usr.toggle@0 Bool)
+    (stopwatch.usr.reset@0 Bool)
+    (stopwatch.usr.count@0 Int)
+    (stopwatch.res.init_flag@0 Bool)
+    (stopwatch.res.abs_0@0 Bool)
+    (stopwatch.impl.usr.running@0 Bool)
+    (stopwatch.res.abs_1@0 Int)
+    (stopwatch.res.inst_0@0 Bool)
+  ) Bool
+  
+  (and
+   (=
+    stopwatch.impl.usr.running@1
+    (not (= stopwatch.impl.usr.running@0 stopwatch.usr.toggle@1)))
+   (=
+    stopwatch.usr.count@1
+    (ite
+     stopwatch.usr.reset@1
+     0
+     (ite
+      stopwatch.impl.usr.running@1
+      (+ stopwatch.res.abs_1@1 1)
+      stopwatch.res.abs_1@1)))
+   (= stopwatch.res.abs_0@1 (>= stopwatch.usr.count@1 0))
+   (__node_trans_previous_0
+    stopwatch.usr.count@1
+    stopwatch.res.abs_1@1
+    stopwatch.res.inst_0@1
+    stopwatch.usr.count@0
+    stopwatch.res.abs_1@0
+    stopwatch.res.inst_0@0)
+   (not stopwatch.res.init_flag@1)
+   true)
+)
+
+
+
+(synth-inv str_invariant(
+  (stopwatch.usr.toggle Bool)
+  (stopwatch.usr.reset Bool)
+  (stopwatch.usr.count Int)
+  (stopwatch.res.init_flag Bool)
+  (stopwatch.res.abs_0 Bool)
+  (stopwatch.impl.usr.running Bool)
+  (stopwatch.res.abs_1 Int)
+  (stopwatch.res.inst_0 Bool)
+))
+
+
+(declare-primed-var stopwatch.usr.toggle Bool)
+(declare-primed-var stopwatch.usr.reset Bool)
+(declare-primed-var stopwatch.usr.count Int)
+(declare-primed-var stopwatch.res.init_flag Bool)
+(declare-primed-var stopwatch.res.abs_0 Bool)
+(declare-primed-var stopwatch.impl.usr.running Bool)
+(declare-primed-var stopwatch.res.abs_1 Int)
+(declare-primed-var stopwatch.res.inst_0 Bool)
+
+(define-fun
+  init (
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+  ) Bool
+  
+  (and
+   (= stopwatch.impl.usr.running (not (not stopwatch.usr.toggle)))
+   (=
+    stopwatch.usr.count
+    (ite
+     stopwatch.usr.reset
+     0
+     (ite
+      stopwatch.impl.usr.running
+      (+ stopwatch.res.abs_1 1)
+      stopwatch.res.abs_1)))
+   (= stopwatch.res.abs_0 (>= stopwatch.usr.count 0))
+   (__node_init_previous_0
+    stopwatch.usr.count
+    stopwatch.res.abs_1
+    stopwatch.res.inst_0)
+   stopwatch.res.init_flag
+   true)
+)
+
+(define-fun
+  trans (
+    
+    ;; Constants.
+    
+    
+    ;; Current state.
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+    
+    ;; Next state.
+    (stopwatch.usr.toggle! Bool)
+    (stopwatch.usr.reset! Bool)
+    (stopwatch.usr.count! Int)
+    (stopwatch.res.init_flag! Bool)
+    (stopwatch.res.abs_0! Bool)
+    (stopwatch.impl.usr.running! Bool)
+    (stopwatch.res.abs_1! Int)
+    (stopwatch.res.inst_0! Bool)
+  
+  ) Bool
+  
+  (and
+   (=
+    stopwatch.impl.usr.running!
+    (not (= stopwatch.impl.usr.running stopwatch.usr.toggle!)))
+   (=
+    stopwatch.usr.count!
+    (ite
+     stopwatch.usr.reset!
+     0
+     (ite
+      stopwatch.impl.usr.running!
+      (+ stopwatch.res.abs_1! 1)
+      stopwatch.res.abs_1!)))
+   (= stopwatch.res.abs_0! (>= stopwatch.usr.count! 0))
+   (__node_trans_previous_0
+    stopwatch.usr.count!
+    stopwatch.res.abs_1!
+    stopwatch.res.inst_0!
+    stopwatch.usr.count
+    stopwatch.res.abs_1
+    stopwatch.res.inst_0)
+   (not stopwatch.res.init_flag!)
+   true)
+)
+
+(define-fun
+  prop (
+    (stopwatch.usr.toggle Bool)
+    (stopwatch.usr.reset Bool)
+    (stopwatch.usr.count Int)
+    (stopwatch.res.init_flag Bool)
+    (stopwatch.res.abs_0 Bool)
+    (stopwatch.impl.usr.running Bool)
+    (stopwatch.res.abs_1 Int)
+    (stopwatch.res.inst_0 Bool)
+  ) Bool
+  
+  stopwatch.res.abs_0
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)