(set-info :smt-lib-version 2.5) (set-logic QF_S) (set-info :status sat) (declare-fun I0_15 () Int) (declare-fun I0_18 () Int) (declare-fun I0_2 () Int) (declare-fun I0_4 () Int) (declare-fun I0_6 () Int) (declare-fun PCTEMP_LHS_1 () Int) (declare-fun PCTEMP_LHS_2 () Int) (declare-fun PCTEMP_LHS_3 () Int) (declare-fun PCTEMP_LHS_4 () Int) (declare-fun PCTEMP_LHS_5 () Int) (declare-fun T0_15 () String) (declare-fun T0_18 () String) (declare-fun T0_2 () String) (declare-fun T0_4 () String) (declare-fun T0_6 () String) (declare-fun T1_15 () String) (declare-fun T1_18 () String) (declare-fun T1_2 () String) (declare-fun T1_4 () String) (declare-fun T1_6 () String) (declare-fun T2_15 () String) (declare-fun T2_18 () String) (declare-fun T2_2 () String) (declare-fun T2_4 () String) (declare-fun T2_6 () String) (declare-fun T3_15 () String) (declare-fun T3_18 () String) (declare-fun T3_2 () String) (declare-fun T3_4 () String) (declare-fun T3_6 () String) (declare-fun T4_15 () String) (declare-fun T4_18 () String) (declare-fun T4_2 () String) (declare-fun T4_4 () String) (declare-fun T4_6 () String) (declare-fun T5_15 () String) (declare-fun T5_18 () String) (declare-fun T5_2 () String) (declare-fun T5_4 () String) (declare-fun T5_6 () String) (declare-fun T_4 () Bool) (declare-fun T_5 () Bool) (declare-fun T_6 () Bool) (declare-fun T_7 () Bool) (declare-fun T_8 () Bool) (declare-fun T_9 () Bool) (declare-fun T_SELECT_1 () Bool) (declare-fun T_SELECT_2 () Bool) (declare-fun T_SELECT_3 () Bool) (declare-fun T_SELECT_4 () Bool) (declare-fun T_SELECT_5 () Bool) (declare-fun T_a () Bool) (declare-fun T_c () Bool) (declare-fun T_e () Bool) (declare-fun var_0xINPUT_12454 () String) (assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1))))) (assert (ite T_SELECT_1 (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))))) (assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1))))) (assert (ite T_SELECT_2 (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) (assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1))))) (assert (ite T_SELECT_3 (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) (assert (= T_4 (<= 0 PCTEMP_LHS_1))) (assert T_4) (assert (= T_5 (<= 0 PCTEMP_LHS_2))) (assert T_5) (assert (= T_6 (<= 0 PCTEMP_LHS_3))) (assert T_6) (assert (= T_7 (= "" var_0xINPUT_12454))) (assert (= T_8 (not T_7))) (assert T_8) (assert (= T_9 (= var_0xINPUT_12454 ""))) (assert (= T_a (not T_9))) (assert T_a) (assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1))))) (assert (ite T_SELECT_4 (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) (assert (= T_c (< (- 1) PCTEMP_LHS_4))) (assert T_c) (assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1))))) (assert (ite T_SELECT_5 (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";")))))) (assert (= T_e (< PCTEMP_LHS_5 0))) (assert T_e) (check-sat)