diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-16 15:37:58 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-16 15:37:58 -0600 |
| commit | 650bb8fecf03c2af1da83177c3ad3f6c1b532294 (patch) | |
| tree | f94917dd435a37830922a2348ad28373811fead8 /test/regress/regress0 | |
| parent | 0619ddd0da84b91218dbef492e1abb09a4558c3f (diff) | |
adds partial functions
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/at001.smt2 | 12 | ||||
| -rw-r--r-- | test/regress/regress0/strings/substr001.smt2 | 1 |
3 files changed, 13 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a5c6ae2f4..a2142eeb3 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + at001.smt2 \ cardinality.smt2 \ str001.smt2 \ str002.smt2 \ diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2 new file mode 100644 index 000000000..855957430 --- /dev/null +++ b/test/regress/regress0/strings/at001.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun i () Int)
+
+(assert (= (str.at x i) "b"))
+(assert (> i 5))
+(assert (< (str.len x) 4))
+(assert (> (str.len x) 2))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 index c0554c481..476b82699 100644 --- a/test/regress/regress0/strings/substr001.smt2 +++ b/test/regress/regress0/strings/substr001.smt2 @@ -1,5 +1,4 @@ (set-logic QF_S)
-(set-option :strings-exp true)
(set-info :status sat)
(declare-fun x () String)
|