Commit c8a598c6 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Move benchmarks from pending repository.

parent 2041aa27
Pipeline #276 failed with stages
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Andrew Reynolds
Generated on: 2018-04-25
Generator: Kudzu, converted to v2.6 by CVC4
Application: Symbolic Execution of Javascript
Target solver: Kaluza
Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun T_1 () Bool)
(declare-fun T_10 () Bool)
(declare-fun T_11 () Bool)
(declare-fun T_12 () Bool)
(declare-fun T_13 () Bool)
(declare-fun T_14 () Bool)
(declare-fun T_15 () Bool)
(declare-fun T_16 () Bool)
(declare-fun T_17 () Bool)
(declare-fun T_18 () Bool)
(declare-fun T_19 () Bool)
(declare-fun T_2 () Bool)
(declare-fun T_3 () Bool)
(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_a () Bool)
(declare-fun T_b () Bool)
(declare-fun T_c () Bool)
(declare-fun T_d () Bool)
(declare-fun T_e () Bool)
(declare-fun T_f () Bool)
(declare-fun var_0xINPUT_41583 () String)
(assert (= T_1 (not (= "qXdHDo7IZR" var_0xINPUT_41583))))
(assert (= T_2 (not T_1)))
(assert T_2)
(assert (= T_3 (not (= "" var_0xINPUT_41583))))
(assert T_3)
(assert (= T_4 (not (= "qXdHDo7IZR" var_0xINPUT_41583))))
(assert (= T_5 (not T_4)))
(assert T_5)
(assert (= T_6 (not (= var_0xINPUT_41583 "qXdHDo7IZR"))))
(assert (= T_7 (not T_6)))
(assert T_7)
(assert (= T_8 (= var_0xINPUT_41583 "")))
(assert (= T_9 (not T_8)))
(assert T_9)
(assert (= T_a (not (= "" var_0xINPUT_41583))))
(assert T_a)
(assert (= T_b (not (= "" var_0xINPUT_41583))))
(assert T_b)
(assert (= T_c (not (= var_0xINPUT_41583 ""))))
(assert T_c)
(assert (= T_d (= var_0xINPUT_41583 "")))
(assert (= T_e (not T_d)))
(assert T_e)
(assert (= T_f (not (= "" var_0xINPUT_41583))))
(assert T_f)
(assert (= T_10 (not (= var_0xINPUT_41583 ""))))
(assert T_10)
(assert (= T_11 (not (= "" var_0xINPUT_41583))))
(assert T_11)
(assert (= T_12 (= var_0xINPUT_41583 "")))
(assert (= T_13 (not T_12)))
(assert T_13)
(assert (= T_14 (not (= "" var_0xINPUT_41583))))
(assert T_14)
(assert (= T_15 (not (= var_0xINPUT_41583 ""))))
(assert T_15)
(assert (= T_16 (not (= "" var_0xINPUT_41583))))
(assert T_16)
(assert (= T_17 (= var_0xINPUT_41583 "")))
(assert (= T_18 (not T_17)))
(assert T_18)
(assert (= T_19 (not (= var_0xINPUT_41583 ""))))
(assert T_19)
(check-sat)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Andrew Reynolds
Generated on: 2018-04-25
Generator: Kudzu, converted to v2.6 by CVC4
Application: Symbolic Execution of Javascript
Target solver: Kaluza
Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun I0_16 () Int)
(declare-fun I0_2 () Int)
(declare-fun I0_21 () Int)
(declare-fun I0_25 () Int)
(declare-fun I0_35 () Int)
(declare-fun I0_4 () Int)
(declare-fun I0_40 () Int)
(declare-fun I0_44 () Int)
(declare-fun I0_54 () Int)
(declare-fun I0_59 () Int)
(declare-fun I0_63 () Int)
(declare-fun I0_73 () Int)
(declare-fun I0_8 () Int)
(declare-fun I1_21 () Int)
(declare-fun I1_25 () Int)
(declare-fun I1_40 () Int)
(declare-fun I1_44 () Int)
(declare-fun I1_59 () Int)
(declare-fun I1_63 () Int)
(declare-fun I1_8 () Int)
(declare-fun I2_21 () Int)
(declare-fun I2_25 () Int)
(declare-fun I2_40 () Int)
(declare-fun I2_44 () Int)
(declare-fun I2_59 () Int)
(declare-fun I2_63 () Int)
(declare-fun I2_8 () Int)
(declare-fun M0_10 () String)
(declare-fun M10_10 () String)
(declare-fun M11_10 () String)
(declare-fun M12_10 () String)
(declare-fun M13_10 () String)
(declare-fun M14_10 () String)
(declare-fun M15_10 () String)
(declare-fun M16_10 () String)
(declare-fun M17_10 () String)
(declare-fun M18_10 () String)
(declare-fun M19_10 () String)
(declare-fun M1_10 () String)
(declare-fun M20_10 () String)
(declare-fun M21_10 () String)
(declare-fun M22_10 () String)
(declare-fun M23_10 () String)
(declare-fun M24_10 () String)
(declare-fun M2_10 () String)
(declare-fun M3_10 () String)
(declare-fun M4_10 () String)
(declare-fun M5_10 () String)
(declare-fun M6_10 () String)
(declare-fun M7_10 () String)
(declare-fun M8_10 () String)
(declare-fun M9_10 () String)
(declare-fun P0_10 () String)
(declare-fun P10_10 () String)
(declare-fun P11_10 () String)
(declare-fun P12_10 () String)
(declare-fun P13_10 () String)
(declare-fun P14_10 () String)
(declare-fun P15_10 () String)
(declare-fun P16_10 () String)
(declare-fun P17_10 () String)
(declare-fun P18_10 () String)
(declare-fun P19_10 () String)
(declare-fun P1_10 () String)
(declare-fun P20_10 () String)
(declare-fun P21_10 () String)
(declare-fun P22_10 () String)
(declare-fun P23_10 () String)
(declare-fun P24_10 () String)
(declare-fun P2_10 () String)
(declare-fun P3_10 () String)
(declare-fun P4_10 () String)
(declare-fun P5_10 () String)
(declare-fun P6_10 () String)
(declare-fun P7_10 () String)
(declare-fun P8_10 () String)
(declare-fun P9_10 () String)
(declare-fun PCTEMP_LHS_1 () Int)
(declare-fun PCTEMP_LHS_10 () Int)
(declare-fun PCTEMP_LHS_11 () String)
(declare-fun PCTEMP_LHS_12 () String)
(declare-fun PCTEMP_LHS_13 () String)
(declare-fun PCTEMP_LHS_14 () String)
(declare-fun PCTEMP_LHS_15 () Int)
(declare-fun PCTEMP_LHS_16 () String)
(declare-fun PCTEMP_LHS_17 () String)
(declare-fun PCTEMP_LHS_18 () String)
(declare-fun PCTEMP_LHS_19 () String)
(declare-fun PCTEMP_LHS_2 () Int)
(declare-fun PCTEMP_LHS_20 () Int)
(declare-fun PCTEMP_LHS_3 () String)
(declare-fun PCTEMP_LHS_4 () String)
(declare-fun PCTEMP_LHS_4_idx_0 () String)
(declare-fun PCTEMP_LHS_4_idx_1 () String)
(declare-fun PCTEMP_LHS_4_idx_10 () String)
(declare-fun PCTEMP_LHS_4_idx_11 () String)
(declare-fun PCTEMP_LHS_4_idx_12 () String)
(declare-fun PCTEMP_LHS_4_idx_13 () String)
(declare-fun PCTEMP_LHS_4_idx_14 () String)
(declare-fun PCTEMP_LHS_4_idx_15 () String)
(declare-fun PCTEMP_LHS_4_idx_16 () String)
(declare-fun PCTEMP_LHS_4_idx_17 () String)
(declare-fun PCTEMP_LHS_4_idx_18 () String)
(declare-fun PCTEMP_LHS_4_idx_19 () String)
(declare-fun PCTEMP_LHS_4_idx_2 () String)
(declare-fun PCTEMP_LHS_4_idx_20 () String)
(declare-fun PCTEMP_LHS_4_idx_21 () String)
(declare-fun PCTEMP_LHS_4_idx_22 () String)
(declare-fun PCTEMP_LHS_4_idx_23 () String)
(declare-fun PCTEMP_LHS_4_idx_24 () String)
(declare-fun PCTEMP_LHS_4_idx_25 () String)
(declare-fun PCTEMP_LHS_4_idx_3 () String)
(declare-fun PCTEMP_LHS_4_idx_4 () String)
(declare-fun PCTEMP_LHS_4_idx_5 () String)
(declare-fun PCTEMP_LHS_4_idx_6 () String)
(declare-fun PCTEMP_LHS_4_idx_7 () String)
(declare-fun PCTEMP_LHS_4_idx_8 () String)
(declare-fun PCTEMP_LHS_4_idx_9 () String)
(declare-fun PCTEMP_LHS_5 () Int)
(declare-fun PCTEMP_LHS_6 () String)
(declare-fun PCTEMP_LHS_7 () String)
(declare-fun PCTEMP_LHS_8 () String)
(declare-fun PCTEMP_LHS_9 () String)
(declare-fun T0_10 () String)
(declare-fun T0_16 () String)
(declare-fun T0_2 () String)
(declare-fun T0_35 () String)
(declare-fun T0_4 () String)
(declare-fun T0_54 () String)
(declare-fun T0_73 () String)
(declare-fun T10_10 () String)
(declare-fun T11_10 () String)
(declare-fun T12_10 () String)
(declare-fun T13_10 () String)
(declare-fun T14_10 () String)
(declare-fun T15_10 () String)
(declare-fun T16_10 () String)
(declare-fun T17_10 () String)
(declare-fun T18_10 () String)
(declare-fun T19_10 () String)
(declare-fun T1_10 () String)
(declare-fun T1_16 () String)
(declare-fun T1_2 () String)
(declare-fun T1_21 () String)
(declare-fun T1_25 () String)
(declare-fun T1_35 () String)
(declare-fun T1_4 () String)
(declare-fun T1_40 () String)
(declare-fun T1_44 () String)
(declare-fun T1_54 () String)
(declare-fun T1_59 () String)
(declare-fun T1_63 () String)
(declare-fun T1_73 () String)
(declare-fun T1_8 () String)
(declare-fun T20_10 () String)
(declare-fun T21_10 () String)
(declare-fun T22_10 () String)
(declare-fun T23_10 () String)
(declare-fun T24_10 () String)
(declare-fun T25_10 () String)
(declare-fun T2_10 () String)
(declare-fun T2_16 () String)
(declare-fun T2_2 () String)
(declare-fun T2_21 () String)
(declare-fun T2_25 () String)
(declare-fun T2_35 () String)
(declare-fun T2_4 () String)
(declare-fun T2_40 () String)
(declare-fun T2_44 () String)
(declare-fun T2_54 () String)
(declare-fun T2_59 () String)
(declare-fun T2_63 () String)
(declare-fun T2_73 () String)
(declare-fun T2_8 () String)
(declare-fun T3_10 () String)
(declare-fun T3_16 () String)
(declare-fun T3_2 () String)
(declare-fun T3_21 () String)
(declare-fun T3_25 () String)
(declare-fun T3_35 () String)
(declare-fun T3_4 () String)
(declare-fun T3_40 () String)
(declare-fun T3_44 () String)
(declare-fun T3_54 () String)
(declare-fun T3_59 () String)
(declare-fun T3_63 () String)
(declare-fun T3_73 () String)
(declare-fun T3_8 () String)
(declare-fun T4_10 () String)
(declare-fun T4_16 () String)
(declare-fun T4_2 () String)
(declare-fun T4_35 () String)
(declare-fun T4_4 () String)
(declare-fun T4_54 () String)
(declare-fun T4_73 () String)
(declare-fun T5_10 () String)
(declare-fun T5_16 () String)
(declare-fun T5_2 () String)
(declare-fun T5_35 () String)
(declare-fun T5_4 () String)
(declare-fun T5_54 () String)
(declare-fun T5_73 () String)
(declare-fun T6_10 () String)
(declare-fun T7_10 () String)
(declare-fun T8_10 () String)
(declare-fun T9_10 () String)
(declare-fun T_10 () Int)
(declare-fun T_14 () Int)
(declare-fun T_15 () Bool)
(declare-fun T_16 () String)
(declare-fun T_18 () Bool)
(declare-fun T_19 () Bool)
(declare-fun T_1a () String)
(declare-fun T_1c () String)
(declare-fun T_1d () Int)
(declare-fun T_21 () Int)
(declare-fun T_22 () Bool)
(declare-fun T_23 () String)
(declare-fun T_25 () Bool)
(declare-fun T_26 () Bool)
(declare-fun T_27 () String)
(declare-fun T_29 () String)
(declare-fun T_2a () Int)
(declare-fun T_2e () Int)
(declare-fun T_2f () Bool)
(declare-fun T_3 () Bool)
(declare-fun T_30 () String)
(declare-fun T_32 () Bool)
(declare-fun T_4 () Int)
(declare-fun T_7 () Int)
(declare-fun T_8 () Bool)
(declare-fun T_9 () String)
(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_SELECT_6 () Bool)
(declare-fun T_b () Bool)
(declare-fun T_c () Bool)
(declare-fun T_d () String)
(declare-fun T_f () String)
(declare-fun var_0xINPUT_212 () String)
(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
(assert (ite T_SELECT_1 (and (= PCTEMP_LHS_1 (+ I0_2 0)) (= var_0xINPUT_212 (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 "?") (not (str.in-re T4_2 (str.to-re "?")))) (and (= PCTEMP_LHS_1 (- 1)) (= var_0xINPUT_212 (str.++ T0_2 T1_2)) (= 0 (str.len T0_2)) (not (str.in-re T1_2 (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_212 (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 "#") (not (str.in-re T4_4 (str.to-re "#")))) (and (= PCTEMP_LHS_2 (- 1)) (= var_0xINPUT_212 (str.++ T0_4 T1_4)) (= 0 (str.len T0_4)) (not (str.in-re T1_4 (str.to-re "#"))))))
(assert (= T_3 (= PCTEMP_LHS_2 (- 1))))
(assert T_3)
(assert (= T_4 (+ PCTEMP_LHS_1 1)))
(assert (= I0_8 (- I2_8 T_4)))
(assert (>= T_4 0))
(assert (>= I2_8 T_4))
(assert (<= I2_8 I1_8))
(assert (= I2_8 I1_8))
(assert (= I0_8 (str.len PCTEMP_LHS_3)))
(assert (= var_0xINPUT_212 (str.++ T1_8 T2_8)))
(assert (= T2_8 (str.++ PCTEMP_LHS_3 T3_8)))
(assert (= T_4 (str.len T1_8)))
(assert (= I1_8 (str.len var_0xINPUT_212)))
(assert (= T25_10 PCTEMP_LHS_4_idx_25))
(assert (= T0_10 PCTEMP_LHS_3))
(assert (= M24_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_24 (str.to-re "&"))))
(assert (= P24_10 (str.++ PCTEMP_LHS_4_idx_24 M24_10)))
(assert (= T24_10 (str.++ P24_10 T25_10)))
(assert (= M23_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_23 (str.to-re "&"))))
(assert (= P23_10 (str.++ PCTEMP_LHS_4_idx_23 M23_10)))
(assert (= T23_10 (str.++ P23_10 T24_10)))
(assert (= M22_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_22 (str.to-re "&"))))
(assert (= P22_10 (str.++ PCTEMP_LHS_4_idx_22 M22_10)))
(assert (= T22_10 (str.++ P22_10 T23_10)))
(assert (= M21_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_21 (str.to-re "&"))))
(assert (= P21_10 (str.++ PCTEMP_LHS_4_idx_21 M21_10)))
(assert (= T21_10 (str.++ P21_10 T22_10)))
(assert (= M20_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_20 (str.to-re "&"))))
(assert (= P20_10 (str.++ PCTEMP_LHS_4_idx_20 M20_10)))
(assert (= T20_10 (str.++ P20_10 T21_10)))
(assert (= M19_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_19 (str.to-re "&"))))
(assert (= P19_10 (str.++ PCTEMP_LHS_4_idx_19 M19_10)))
(assert (= T19_10 (str.++ P19_10 T20_10)))
(assert (= M18_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_18 (str.to-re "&"))))
(assert (= P18_10 (str.++ PCTEMP_LHS_4_idx_18 M18_10)))
(assert (= T18_10 (str.++ P18_10 T19_10)))
(assert (= M17_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_17 (str.to-re "&"))))
(assert (= P17_10 (str.++ PCTEMP_LHS_4_idx_17 M17_10)))
(assert (= T17_10 (str.++ P17_10 T18_10)))
(assert (= M16_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_16 (str.to-re "&"))))
(assert (= P16_10 (str.++ PCTEMP_LHS_4_idx_16 M16_10)))
(assert (= T16_10 (str.++ P16_10 T17_10)))
(assert (= M15_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_15 (str.to-re "&"))))
(assert (= P15_10 (str.++ PCTEMP_LHS_4_idx_15 M15_10)))
(assert (= T15_10 (str.++ P15_10 T16_10)))
(assert (= M14_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_14 (str.to-re "&"))))
(assert (= P14_10 (str.++ PCTEMP_LHS_4_idx_14 M14_10)))
(assert (= T14_10 (str.++ P14_10 T15_10)))
(assert (= M13_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_13 (str.to-re "&"))))
(assert (= P13_10 (str.++ PCTEMP_LHS_4_idx_13 M13_10)))
(assert (= T13_10 (str.++ P13_10 T14_10)))
(assert (= M12_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_12 (str.to-re "&"))))
(assert (= P12_10 (str.++ PCTEMP_LHS_4_idx_12 M12_10)))
(assert (= T12_10 (str.++ P12_10 T13_10)))
(assert (= M11_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_11 (str.to-re "&"))))
(assert (= P11_10 (str.++ PCTEMP_LHS_4_idx_11 M11_10)))
(assert (= T11_10 (str.++ P11_10 T12_10)))
(assert (= M10_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_10 (str.to-re "&"))))
(assert (= P10_10 (str.++ PCTEMP_LHS_4_idx_10 M10_10)))
(assert (= T10_10 (str.++ P10_10 T11_10)))
(assert (= M9_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_9 (str.to-re "&"))))
(assert (= P9_10 (str.++ PCTEMP_LHS_4_idx_9 M9_10)))
(assert (= T9_10 (str.++ P9_10 T10_10)))
(assert (= M8_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_8 (str.to-re "&"))))
(assert (= P8_10 (str.++ PCTEMP_LHS_4_idx_8 M8_10)))
(assert (= T8_10 (str.++ P8_10 T9_10)))
(assert (= M7_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_7 (str.to-re "&"))))
(assert (= P7_10 (str.++ PCTEMP_LHS_4_idx_7 M7_10)))
(assert (= T7_10 (str.++ P7_10 T8_10)))
(assert (= M6_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_6 (str.to-re "&"))))
(assert (= P6_10 (str.++ PCTEMP_LHS_4_idx_6 M6_10)))
(assert (= T6_10 (str.++ P6_10 T7_10)))
(assert (= M5_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_5 (str.to-re "&"))))
(assert (= P5_10 (str.++ PCTEMP_LHS_4_idx_5 M5_10)))
(assert (= T5_10 (str.++ P5_10 T6_10)))
(assert (= M4_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_4 (str.to-re "&"))))
(assert (= P4_10 (str.++ PCTEMP_LHS_4_idx_4 M4_10)))
(assert (= T4_10 (str.++ P4_10 T5_10)))
(assert (= M3_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_3 (str.to-re "&"))))
(assert (= P3_10 (str.++ PCTEMP_LHS_4_idx_3 M3_10)))
(assert (= T3_10 (str.++ P3_10 T4_10)))
(assert (= M2_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_2 (str.to-re "&"))))
(assert (= P2_10 (str.++ PCTEMP_LHS_4_idx_2 M2_10)))
(assert (= T2_10 (str.++ P2_10 T3_10)))
(assert (= M1_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_1 (str.to-re "&"))))
(assert (= P1_10 (str.++ PCTEMP_LHS_4_idx_1 M1_10)))
(assert (= T1_10 (str.++ P1_10 T2_10)))
(assert (= M0_10 "&"))
(assert (not (str.in-re PCTEMP_LHS_4_idx_0 (str.to-re "&"))))
(assert (= P0_10 (str.++ PCTEMP_LHS_4_idx_0 M0_10)))
(assert (= T0_10 (str.++ P0_10 T1_10)))
(assert (= T_7 (str.len PCTEMP_LHS_4)))
(assert (= T_8 (< 0 T_7)))
(assert T_8)
(assert (= T_9 PCTEMP_LHS_4_idx_0))
(assert (= T_SELECT_3 (not (= PCTEMP_LHS_5 (- 1)))))
(assert (ite T_SELECT_3 (and (= PCTEMP_LHS_5 (+ I0_16 0)) (= T_9 (str.++ T0_16 T1_16)) (= I0_16 (str.len T4_16)) (= 0 (str.len T0_16)) (= T1_16 (str.++ T2_16 T3_16)) (= T2_16 (str.++ T4_16 T5_16)) (= T5_16 "=") (not (str.in-re T4_16 (str.to-re "=")))) (and (= PCTEMP_LHS_5 (- 1)) (= T_9 (str.++ T0_16 T1_16)) (= 0 (str.len T0_16)) (not (str.in-re T1_16 (str.to-re "="))))))
(assert (= T_b (= PCTEMP_LHS_5 (- 1))))
(assert (= T_c (not T_b)))
(assert T_c)
(assert (= T_d PCTEMP_LHS_4_idx_0))
(assert (= I0_21 (- PCTEMP_LHS_5 0)))
(assert (>= 0 0))
(assert (>= PCTEMP_LHS_5 0))
(assert (<= PCTEMP_LHS_5 I1_21))
(assert (= I2_21 I1_21))
(assert (= I0_21 (str.len PCTEMP_LHS_6)))
(assert (= T_d (str.++ T1_21 T2_21)))
(assert (= T2_21 (str.++ PCTEMP_LHS_6 T3_21)))
(assert (= 0 (str.len T1_21)))
(assert (= I1_21 (str.len T_d)))
(assert (= T_f PCTEMP_LHS_4_idx_0))
(assert (= T_10 (+ PCTEMP_LHS_5 1)))
(assert (= I0_25 (- I2_25 T_10)))
(assert (>= T_10 0))
(assert (>= I2_25 T_10))
(assert (<= I2_25 I1_25))
(assert (= I2_25 I1_25))
(assert (= I0_25 (str.len PCTEMP_LHS_7)))
(assert (= T_f (str.++ T1_25 T2_25)))
(assert (= T2_25 (str.++ PCTEMP_LHS_7 T3_25)))
(assert (= T_10 (str.len T1_25)))
(assert (= I1_25 (str.len T_f)))
(assert (not (str.in-re PCTEMP_LHS_8 (str.to-re "+"))))
(assert (= PCTEMP_LHS_8 PCTEMP_LHS_7))
(assert (= PCTEMP_LHS_9 PCTEMP_LHS_8))
(assert (not (str.in-re PCTEMP_LHS_9 (str.to-re "%"))))
(assert (= T_14 (str.len PCTEMP_LHS_4)))
(assert (= T_15 (< 1 T_14)))
(assert T_15)
(assert (= T_16 PCTEMP_LHS_4_idx_1))
(assert (= T_SELECT_4 (not (= PCTEMP_LHS_10 (- 1)))))
(assert (ite T_SELECT_4 (and (= PCTEMP_LHS_10 (+ I0_35 0)) (= T_16 (str.++ T0_35 T1_35)) (= I0_35 (str.len T4_35)) (= 0 (str.len T0_35)) (= T1_35 (str.++ T2_35 T3_35)) (= T2_35 (str.++ T4_35 T5_35)) (= T5_35 "=") (not (str.in-re T4_35 (str.to-re "=")))) (and (= PCTEMP_LHS_10 (- 1)) (= T_16 (str.++ T0_35 T1_35)) (= 0 (str.len T0_35)) (not (str.in-re T1_35 (str.to-re "="))))))
(assert (= T_18 (= PCTEMP_LHS_10 (- 1))))
(assert (= T_19 (not T_18)))
(assert T_19)
(assert (= T_1a PCTEMP_LHS_4_idx_1))
(assert (= I0_40 (- PCTEMP_LHS_10 0)))
(assert (>= 0 0))
(assert (>= PCTEMP_LHS_10 0))
(assert (<= PCTEMP_LHS_10 I1_40))
(assert (= I2_40 I1_40))
(assert (= I0_40 (str.len PCTEMP_LHS_11)))
(assert (= T_1a (str.++ T1_40 T2_40)))
(assert (= T2_40 (str.++ PCTEMP_LHS_11 T3_40)))
(assert (= 0 (str.len T1_40)))
(assert (= I1_40 (str.len T_1a)))
(assert (= T_1c PCTEMP_LHS_4_idx_1))
(assert (= T_1d (+ PCTEMP_LHS_10 1)))
(assert (= I0_44 (- I2_44 T_1d)))
(assert (>= T_1d 0))
(assert (>= I2_44 T_1d))
(assert (<= I2_44 I1_44))
(assert (= I2_44 I1_44))
(assert (= I0_44 (str.len PCTEMP_LHS_12)))
(assert (= T_1c (str.++ T1_44 T2_44)))
(assert (= T2_44 (str.++ PCTEMP_LHS_12 T3_44)))
(assert (= T_1d (str.len T1_44)))
(assert (= I1_44 (str.len T_1c)))
(assert (not (str.in-re PCTEMP_LHS_13 (str.to-re "+"))))
(assert (= PCTEMP_LHS_13 PCTEMP_LHS_12))
(assert (= PCTEMP_LHS_14 PCTEMP_LHS_13))
(assert (not (str.in-re PCTEMP_LHS_14 (str.to-re "%"))))
(assert (= T_21 (str.len PCTEMP_LHS_4)))
(assert (= T_22 (< 2 T_21)))
(assert T_22)
(assert (= T_23 PCTEMP_LHS_4_idx_2))
(assert (= T_SELECT_5 (not (= PCTEMP_LHS_15 (- 1)))))
(assert (ite T_SELECT_5 (and (= PCTEMP_LHS_15 (+ I0_54 0)) (= T_23 (str.++ T0_54 T1_54)) (= I0_54 (str.len T4_54)) (= 0 (str.len T0_54)) (= T1_54 (str.++ T2_54 T3_54)) (= T2_54 (str.++ T4_54 T5_54)) (= T5_54 "=") (not (str.in-re T4_54 (str.to-re "=")))) (and (= PCTEMP_LHS_15 (- 1)) (= T_23 (str.++ T0_54 T1_54)) (= 0 (str.len T0_54)) (not (str.in-re T1_54 (str.to-re "="))))))
(assert (= T_25 (= PCTEMP_LHS_15 (- 1))))
(assert (= T_26 (not T_25)))
(assert T_26)
(assert (= T_27 PCTEMP_LHS_4_idx_2))
(assert (= I0_59 (- PCTEMP_LHS_15 0)))
(assert (>= 0 0))
(assert (>= PCTEMP_LHS_15 0))
(assert (<= PCTEMP_LHS_15 I1_59))
(assert (= I2_59 I1_59))
(assert (= I0_59 (str.len PCTEMP_LHS_16)))
(assert (= T_27 (str.++ T1_59 T2_59)))
(assert (= T2_59 (str.++ PCTEMP_LHS_16 T3_59)))
(assert (= 0 (str.len T1_59)))
(assert (= I1_59 (str.len T_27)))
(assert (= T_29 PCTEMP_LHS_4_idx_2))
(assert (= T_2a (+ PCTEMP_LHS_15 1)))
(assert (= I0_63 (- I2_63 T_2a)))
(assert (>= T_2a 0))
(assert (>= I2_63 T_2a))
(assert (<= I2_63 I1_63))
(assert (= I2_63 I1_63))
(assert (= I0_63 (str.len PCTEMP_LHS_17)))
(assert (= T_29 (str.++ T1_63 T2_63)))
(assert (= T2_63 (str.++ PCTEMP_LHS_17 T3_63)))
(assert (= T_2a (str.len T1_63)))
(assert (= I1_63 (str.len T_29)))
(assert (not (str.in-re PCTEMP_LHS_18 (str.to-re "+"))))
(assert (= PCTEMP_LHS_18 PCTEMP_LHS_17))
(assert (= PCTEMP_LHS_19 PCTEMP_LHS_18))
(assert (not (str.in-re PCTEMP_LHS_19 (str.to-re "%"))))
(assert (= T_2e (str.len PCTEMP_LHS_4)))
(assert (= T_2f (< 3 T_2e)))
(assert T_2f)
(assert (= T_30 PCTEMP_LHS_4_idx_3))
(assert (= T_SELECT_6 (not (= PCTEMP_LHS_20 (- 1)))))
(assert (ite T_SELECT_6 (and (= PCTEMP_LHS_20 (+ I0_73 0)) (= T_30 (str.++ T0_73 T1_73)) (= I0_73 (str.len T4_73)) (= 0 (str.len T0_73)) (= T1_73 (str.++ T2_73 T3_73)) (= T2_73 (str.++ T4_73 T5_73)) (= T5_73 "=") (not (str.in-re T4_73 (str.to-re "=")))) (and (= PCTEMP_LHS_20 (- 1)) (= T_30 (str.++ T0_73 T1_73)) (= 0 (str.len T0_73)) (not (str.in-re T1_73 (str.to-re "="))))))
(assert (= T_32 (= PCTEMP_LHS_20 (- 1))))
(assert T_32)
(check-sat)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Andrew Reynolds
Generated on: 2018-04-25
Generator: Kudzu, converted to v2.6 by CVC4
Application: Symbolic Execution of Javascript
Target solver: Kaluza
Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun I0_16 () Int)
(declare-fun I0_2 () Int)
(declare-fun I0_21 () Int)
(declare-fun I0_25 () Int)
(declare-fun I0_35 () Int)
(declare-fun I0_4 () Int)
(declare-fun I0_40 () Int)
(declare-fun I0_44 () Int)
(declare-fun I0_54 () Int)
(declare-fun I0_59 () Int)
(declare-fun I0_63 () Int)
(declare-fun I0_73 () Int)
(declare-fun I0_8 () Int)
(declare-fun I1_21 () Int)