diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 22:09:38 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-11-26 22:09:38 -0600 |
commit | 388a6acf4acd50a7611faae91b3489ac2209e584 (patch) | |
tree | 481b5e06632ead33c41d683357e6f0767d7a8479 /test/regress/regress0/strings | |
parent | 02dd486ff30041764da04a016b0abdc75a6a3d93 (diff) |
add intersection rewriting
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)
|