diff options
Diffstat (limited to 'test/regress/regress0/strings')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/regexp003.smt2 | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index c15e93cd8..865d05cd2 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ + regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ loop002.smt2 \ diff --git a/test/regress/regress0/strings/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2 new file mode 100644 index 000000000..601689958 --- /dev/null +++ b/test/regress/regress0/strings/regexp003.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-const s String)
+
+(assert (str.in.re s (re.inter
+ (re.++ (str.to.re "a") (re.* (str.to.re "b"))
+ (re.inter (str.to.re "c") (re.* (str.to.re "c"))))
+ (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
+ )))
+
+(check-sat)
|