diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/pattern1.smt2 | 73 |
2 files changed, 74 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5dd456b9f..5b3f3b729 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2280,6 +2280,7 @@ set(regress_1_tests regress1/strings/nt6-dd.smt2 regress1/strings/nterm-re-inter-sigma.smt2 regress1/strings/open-pf-merge.smt2 + regress1/strings/pattern1.smt2 regress1/strings/pierre150331.smt2 regress1/strings/policy_variable.smt2 regress1/strings/pre_ctn_no_skolem_share.smt2 diff --git a/test/regress/regress1/strings/pattern1.smt2 b/test/regress/regress1/strings/pattern1.smt2 new file mode 100644 index 000000000..b75fdb9be --- /dev/null +++ b/test/regress/regress1/strings/pattern1.smt2 @@ -0,0 +1,73 @@ +(set-option :produce-models true) +(set-logic QF_SLIA) +(set-info :status sat) +(declare-const x String) + +(assert + (str.in_re + x + (re.++ + (str.to_re "pref") + (re.* re.allchar) + (str.to_re "a") + (re.* re.allchar) + (str.to_re "b") + (re.* re.allchar) + (str.to_re "c") + (re.* re.allchar) + (str.to_re "d") + (re.* re.allchar) + (str.to_re "e") + (re.* re.allchar) + (str.to_re "f") + (re.* re.allchar) + (str.to_re "g") + (re.* re.allchar) + (str.to_re "h") + (re.* re.allchar) + (str.to_re "i") + (re.* re.allchar) + (str.to_re "j") + (re.* re.allchar) + (str.to_re "k") + (re.* re.allchar) + (str.to_re "l") + (re.* re.allchar) + (str.to_re "m") + (re.* re.allchar) + (str.to_re "n") + (re.* re.allchar) + (str.to_re "o") + (re.* re.allchar) + (str.to_re "p") + (re.* re.allchar) + (str.to_re "q") + (re.* re.allchar) + (str.to_re "r") + (re.* re.allchar) + (str.to_re "s") + (re.* re.allchar) + (str.to_re "t") + (re.* re.allchar) + (str.to_re "u") + (re.* re.allchar) + (str.to_re "v") + (re.* re.allchar) + (str.to_re "w") + (re.* re.allchar) + (str.to_re "x") + (re.* re.allchar) + (str.to_re "y") + (re.* re.allchar) + (str.to_re "z") + (re.* re.allchar)))) + +(assert + (or + (= x "pref0a-b-c-de") + (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar))) + (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar))))) + +(check-sat) + + |