diff options
Diffstat (limited to 'test/regress/regress0/strings/kaluza-fl.smt2')
| -rw-r--r-- | test/regress/regress0/strings/kaluza-fl.smt2 | 97 |
1 files changed, 0 insertions, 97 deletions
diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2 deleted file mode 100644 index 04775d61c..000000000 --- a/test/regress/regress0/strings/kaluza-fl.smt2 +++ /dev/null @@ -1,97 +0,0 @@ -(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) |