SMT2 string tests for nondet strings

regression/smt2_strings/concat_input_sat/concat_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+concat_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/concat_input_sat/concat_input_sat.smt2

@@ -0,0 +1,5 @@
+(declare-const a String)
+(declare-const b String)
+(declare-const c String)
+(assert (= (str.++ a "cd" b c) "abcdefgh"))
+(check-sat)

regression/smt2_strings/concat_input_unsat/concat_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+concat_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/concat_input_unsat/concat_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const a String)
+(declare-const b String)
+(declare-const c String)
+(assert (= (str.++ a "dc" b c) "abcdefgh"))
+(check-sat)

regression/smt2_strings/contains_input_sat/contains_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+contains_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/contains_input_sat/contains_input_sat.smt2

@@ -0,0 +1,7 @@
+(declare-const needle String)
+(declare-const haystack String)
+(assert (> (str.len needle) 3))
+(assert (> (str.len haystack) 10))
+(assert (not (= needle haystack)))
+(assert (str.contains haystack needle))
+(check-sat)

regression/smt2_strings/contains_input_unsat/contains_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+contains_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/contains_input_unsat/contains_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const needle String)
+(declare-const haystack String)
+(assert (< (str.len haystack) (str.len needle)))
+(assert (str.contains haystack needle))
+(check-sat)

regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+indexof_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/indexof_input_sat/indexof_input_sat.smt2

@@ -0,0 +1,8 @@
+(declare-const haystack String)
+(declare-const needle String)
+(declare-const start Int)
+(declare-const index Int)
+(assert (> index 3))
+(assert (> (str.len needle) 0))
+(assert (= (str.indexof haystack needle start) index))
+(check-sat)

regression/smt2_strings/indexof_input_unsat/indexof_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+indexof_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/indexof_input_unsat/indexof_input_unsat.smt2

@@ -0,0 +1,8 @@
+(declare-const haystack String)
+(declare-const needle String)
+(declare-const start Int)
+(declare-const index Int)
+(assert (< index start))
+(assert (> index 0))
+(assert (= (str.indexof haystack needle start) index))
+(check-sat)

regression/smt2_strings/int_to_str_input_sat/int_to_str_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+int_to_str_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/int_to_str_input_sat/int_to_str_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const str String)
+(declare-const number Int)
+(assert (= (int.to.str number) str))
+(check-sat)

regression/smt2_strings/int_to_str_input_unsat/int_to_str_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+int_to_str_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/int_to_str_input_unsat/int_to_str_input_unsat.smt2

@@ -0,0 +1,6 @@
+(declare-const str String)
+(declare-const number Int)
+(assert (< (str.len str) 4))
+(assert (> number 10000))
+(assert (= (int.to.str number) str))
+(check-sat)

regression/smt2_strings/length_input_sat/length_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+length_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/length_input_sat/length_input_sat.smt2

@@ -0,0 +1,3 @@
+(declare-const str String)
+(assert (= (str.len str) 3))
+(check-sat)

regression/smt2_strings/length_input_unsat/length_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+length_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/length_input_unsat/length_input_unsat.smt2

@@ -0,0 +1,4 @@
+(declare-const str String)
+(assert (= (str.len str) 3))
+(assert (= (str.len str) 2))
+(check-sat)

regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+lex_order_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in String)
+(assert (> (str.len in) 1))
+(assert (str.< in "acc"))
+(check-sat)

regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+lex_order_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.< in1 in2))
+(assert (str.< in2 in1))
+(check-sat)

regression/smt2_strings/prefixof_input_sat/prefixof_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+prefixof_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/prefixof_input_sat/prefixof_input_sat.smt2

@@ -0,0 +1,6 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (not (= in1 in2)))
+(assert (> (str.len in1) 3))
+(assert (str.prefixof in1 in2))
+(check-sat)

regression/smt2_strings/prefixof_input_unsat/prefixof_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+prefixof_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/prefixof_input_unsat/prefixof_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (< (str.len in2) (str.len in1)))
+(assert (str.prefixof in1 in2))
+(check-sat)

regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+reflexive_lex_order_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.smt2

@@ -0,0 +1,6 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (not (= in1 in2)))
+(assert (> (str.len in1) 3))
+(assert (str.<= in1 in2))
+(check-sat)

regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+reflexive_lex_order_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.smt2

@@ -0,0 +1,6 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (= in1 "def"))
+(assert (= in2 "abc"))
+(assert (str.<= in1 in2))
+(check-sat)

regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_concat_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re in1)) (re.* (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_concat_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "abc" (re.++ (re.* (str.to.re in1)) (re.* (str.to.re in2)))))
+(assert (str.in.re "ab" (re.++ (re.* (str.to.re in1)) (re.* (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_inter_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "abc" (re.inter (re.+ (str.to.re in1)) (re.+ (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_inter_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (not (= in1 in2)))
+(assert (str.in.re "abc" (re.inter (re.+ (str.to.re in1)) (re.+ (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_loop_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const lower Int)
+(declare-const upper Int)
+(assert (str.in.re "aaa" ((_ re.loop lower upper) (str.to.re "a"))))
+(check-sat)

regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_loop_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.smt2

@@ -0,0 +1,4 @@
+(declare-const bound Int)
+(assert (> bound 3))
+(assert (str.in.re "aaa" ((_ re.loop bound bound) (str.to.re "a"))))
+(check-sat)

regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_opt_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "aaab" (re.++ (re.+ (str.to.re in1)) (re.opt (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_plus_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "aaabbb" (re.++ (re.+ (str.to.re in1)) (re.+ (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_plus_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.smt2

@@ -0,0 +1,3 @@
+(declare-const in String)
+(assert (str.in.re "aabb" (re.++ (re.+ (str.to.re in)) (re.+ (str.to.re in)))))
+(check-sat)

regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_range_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const lower String)
+(declare-const upper String)
+(assert (str.in.re "c" (re.range lower upper)))
+(check-sat)

regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_range_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const lower String)
+(declare-const upper String)
+(assert (str.in.re "c" (re.range lower upper)))
+(assert (str.in.re "d" (re.range upper lower)))
+(check-sat)

regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_star_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re in1)) (re.* (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_union_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "ab" (re.union (str.to.re in1) (str.to.re in2))))
+(check-sat)

regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+regexp_union_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.smt2

@@ -0,0 +1,6 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (< (str.len in1) 3))
+(assert (< (str.len in2) 3))
+(assert (str.in.re "abcd" (re.union (str.to.re in1) (str.to.re in2))))
+(check-sat)

regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+replace_all_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.smt2

@@ -0,0 +1,9 @@
+(declare-const container String)
+(declare-const target String)
+(declare-const replacement String)
+(assert (< (str.len target) (str.len container)))
+(assert (> (str.len replacement) 2))
+(define-fun replaced () String (str.replaceall container target replacement))
+(assert (= replaced "axydefaxydef"))
+(assert (not (= replaced container)))
+(check-sat)

regression/smt2_strings/replace_input_sat/replace_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+replace_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/replace_input_sat/replace_input_sat.smt2

@@ -0,0 +1,8 @@
+(declare-const container String)
+(declare-const target String)
+(declare-const replacement String)
+(assert (< (str.len target) (str.len container)))
+(assert (> (str.len replacement) 2))
+(define-fun replaced () String (str.replace container target replacement))
+(assert (= replaced "axydefabcdef"))
+(check-sat)

regression/smt2_strings/str_at_input_sat/str_at_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_at_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/str_at_input_sat/str_at_input_sat.smt2

@@ -0,0 +1,5 @@
+(declare-const str String)
+(declare-const index Int)
+(assert (> index 4))
+(assert (= (str.at str index) "c"))
+(check-sat)

regression/smt2_strings/str_at_input_unsat/str_at_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_at_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/str_at_input_unsat/str_at_input_unsat.smt2

@@ -0,0 +1,6 @@
+(declare-const str String)
+(declare-const index Int)
+(assert (> index 4))
+(assert (= (str.at str index) "c"))
+(assert (= (str.at str index) "d"))
+(check-sat)

regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_in_re_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.smt2

@@ -0,0 +1,6 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (> (str.len in1) 3))
+(assert (> (str.len in2) 3))
+(assert (str.in.re in1 (str.to.re in2)))
+(check-sat)

regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_in_re_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.smt2

@@ -0,0 +1,7 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (> (str.len in1) 3))
+(assert (> (str.len in2) 3))
+(assert (not (= in1 in2)))
+(assert (str.in.re in1 (str.to.re in2)))
+(check-sat)

regression/smt2_strings/str_to_int_input_sat/str_to_int_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_to_int_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/str_to_int_input_sat/str_to_int_input_sat.smt2

@@ -0,0 +1,3 @@
+(declare-const in String)
+(assert (= (str.to.int in) 123))
+(check-sat)

regression/smt2_strings/str_to_int_input_unsat/str_to_int_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_to_int_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/str_to_int_input_unsat/str_to_int_input_unsat.smt2

@@ -0,0 +1,4 @@
+(declare-const in String)
+(assert (= (str.to.int in) 123))
+(assert (= (str.to.int in) 1234))
+(check-sat)

regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_to_re_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in1 String)
+(declare-const in2 String)
+(assert (str.in.re "abba" (re.* (re.union (str.to.re in1) (str.to.re in2)))))
+(check-sat)

regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+str_to_re_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.smt2

@@ -0,0 +1,4 @@
+(declare-const in String)
+(assert (str.in.re "abba" (re.+ (str.to.re in))))
+(assert (str.in.re "cddc" (re.+ (str.to.re in))))
+(check-sat)

regression/smt2_strings/substr_input_sat/substr_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+substr_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/substr_input_sat/substr_input_sat.smt2

@@ -0,0 +1,8 @@
+(declare-const str String)
+(declare-const lower Int)
+(declare-const upper Int)
+(assert (< lower upper))
+(define-fun substr () String (str.substr str lower upper))
+(assert (= substr "cde"))
+(assert (not (= str substr)))
+(check-sat)

regression/smt2_strings/substr_input_unsat/substr_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+substr_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/substr_input_unsat/substr_input_unsat.smt2

@@ -0,0 +1,9 @@
+(declare-const str String)
+(declare-const lower Int)
+(declare-const upper Int)
+(assert (< lower upper))
+(define-fun substr () String (str.substr str lower upper))
+(assert (= substr "cde"))
+(assert (= (str.substr str upper lower) "cde"))
+(assert (not (= str substr)))
+(check-sat)

regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.desc

@@ -0,0 +1,8 @@
+FUTURE
+suffixof_input_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.smt2

@@ -0,0 +1,7 @@
+(declare-const str String)
+(declare-const suffix String)
+(assert (> (str.len suffix) 3))
+(assert (not (= str suffix)))
+(assert (str.suffixof suffix str))
+(check-sat)
+(get-model)

regression/smt2_strings/suffixof_input_unsat/suffixof_input_unsat.desc

@@ -0,0 +1,8 @@
+FUTURE
+suffixof_input_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/suffixof_input_unsat/suffixof_input_unsat.smt2

@@ -0,0 +1,5 @@
+(declare-const str String)
+(declare-const suffix String)
+(assert (< (str.len str) (str.len suffix)))
+(assert (str.suffixof suffix str))
+(check-sat)