diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/regexp-native-simple.cvc | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 194dbd663..4b7e9d7ce 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -869,6 +869,7 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/re.all.smt2 + regress0/strings/regexp-native-simple.cvc regress0/strings/regexp_inclusion.smt2 regress0/strings/regexp_inclusion_reduction.smt2 regress0/strings/repl-rewrites2.smt2 diff --git a/test/regress/regress0/strings/regexp-native-simple.cvc b/test/regress/regress0/strings/regexp-native-simple.cvc new file mode 100644 index 000000000..49d6f3d64 --- /dev/null +++ b/test/regress/regress0/strings/regexp-native-simple.cvc @@ -0,0 +1,13 @@ +% EXPECT: sat + +x : STRING; + +ASSERT x IS_IN RE_CONCAT(RE_OPT(RE_STAR(RE_UNION(RE_RANGE("i", "j"), RE_RANGE("k", "l")))), + RE_PLUS(STRING_TO_REGEXP("abc")), + RE_LOOP(STRING_TO_REGEXP("def"), 1, 2), + RE_SIGMA); +ASSERT NOT(x IS_IN RE_INTER(RE_STAR(RE_SIGMA), RE_EMPTY)); + +ASSERT x = "ikljabcabcdefe"; + +CHECKSAT; |