diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-20 21:25:57 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-20 21:28:48 -0500 |
| commit | 60aab6e5b7dde21603eb039f37921614d4424d59 (patch) | |
| tree | 82636da4881edfbe2a059984557e193de0e1f7da /test/regress | |
| parent | 2f4925e3d366bf58437025e0a5b238468e6514f8 (diff) | |
adds regular expression range
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/fmf002.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index ffbfb077d..cd3116eac 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,6 +27,7 @@ TESTS = \ str005.smt2 \ str006.smt2 \ fmf001.smt2 \ + fmf002.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 new file mode 100644 index 000000000..14f50c710 --- /dev/null +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_S)
+(set-option :fmf-strings true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (str.in.re x
+ (re.+ (re.range "a" "c"))
+ ))
+
+(assert (= x (str.++ y "c" z "b")))
+(assert (> (str.len z) 1))
+
+(check-sat)
|