Skip to content

Commit 361050f

Browse files
author
Joel Allred
committed
Add FUTURE tests for SMT2 string operations
1 parent ce6e9b0 commit 361050f

File tree

108 files changed

+540
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

108 files changed

+540
-0
lines changed

‎regression/smt2_strings/concat_const_sat/concat_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
concat_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/concat_const_sat/concat_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.++ "abc" "def" "" "gh") "abcdefgh"))
2+
(check-sat)

‎regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
concat_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.++ "abc" "cdef") "abcde"))
2+
(check-sat)

‎regression/smt2_strings/contains_const_sat/contains_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
contains_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/contains_const_sat/contains_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.contains "abcdef" "bcd"))
2+
(check-sat)

‎regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
contains_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.contains "abcdef" "dc"))
2+
(check-sat)

‎regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
indexof_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.indexof "abcdef" "cde" 1) 2))
2+
(check-sat)

‎regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
indexof_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.indexof "abcdef" "cde" 1) 1))
2+
(check-sat)

‎regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
int_to_str_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (int.to.str 1234567890) "1234567890"))
2+
(check-sat)

‎regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
int_to_str_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (int.to.str 1234567890) "1234467890"))
2+
(check-sat)

‎regression/smt2_strings/length_const_sat/length_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
length_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/length_const_sat/length_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.len "abc") 3))
2+
(check-sat)

‎regression/smt2_strings/length_const_unsat/length_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
length_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/length_const_unsat/length_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (= (str.len "abc") 4))
2+
(check-sat)

‎regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
lex_order_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.< "abc" "acc"))
2+
(check-sat)

‎regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
lex_order_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.< "abc" "aac"))
2+
(check-sat)

‎regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
prefixof_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.prefixof "abc" "abcdef"))
2+
(check-sat)

‎regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
prefixof_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.prefixof "bc" "abcdef"))
2+
(check-sat)

‎regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
reflexive_lex_order_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.<= "abc" "acc"))
2+
(check-sat)

‎regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
reflexive_lex_order_const_sat2.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.<= "abc" "abc"))
2+
(check-sat)

‎regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
reflexive_lex_order_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.<= "acc" "abc"))
2+
(check-sat)

‎regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_all_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "abc" (re.* re.all)))
2+
(check-sat)

‎regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_allchar_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* re.allchar))))
2+
(check-sat)

‎regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_allchar_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "a" (re.++ (re.+ (str.to.re "a")) (re.+ re.allchar))))
2+
(check-sat)

‎regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_concat_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_concat_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaabbbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_inter_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "e" (re.inter (re.range "a" "h") (re.range "d" "w"))))
2+
(check-sat)

‎regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_inter_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "e" (re.inter (re.range "a" "b") (re.range "b" "w"))))
2+
(check-sat)

‎regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_loop_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaa" ((_ re.loop 3 3) (str.to.re "a"))))
2+
(check-sat)

‎regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_loop_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaa" ((_ re.loop 1 2) (str.to.re "a"))))
2+
(check-sat)

‎regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_nostr_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "a" re.nostr))
2+
(check-sat)

‎regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_opt_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaab" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_opt_const_sat2.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaa" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_opt_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaac" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_plus_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaabbb" (re.++ (re.+ (str.to.re "a")) (re.+ (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_plus_const_unsat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--
8+
error

‎regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "aaa" (re.++ (re.+ (str.to.re "a")) (re.+ (str.to.re "b")))))
2+
(check-sat)

‎regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
regexp_range_const_sat.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
8+
error

‎regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.smt2

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
(assert (str.in.re "c" (re.range "a" "f")))
2+
(check-sat)

0 commit comments

Comments
 (0)