diff options
Diffstat (limited to 'test/regress/regress0/strings/kaluza-fl.smt2')
-rwxr-xr-x | test/regress/regress0/strings/kaluza-fl.smt2 | 194 |
1 files changed, 97 insertions, 97 deletions
diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2 index ce3af9e74..04775d61c 100755 --- a/test/regress/regress0/strings/kaluza-fl.smt2 +++ b/test/regress/regress0/strings/kaluza-fl.smt2 @@ -1,97 +1,97 @@ -(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)
+(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) |