diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-27 09:24:42 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-27 09:25:52 -0500 |
commit | 232728df0bb2bc101862cd78c666dfa5ef4ebfe9 (patch) | |
tree | ee0c4800b4c0c71c9f1ae2670925df1dc60f75f9 /test/regress/regress0/strings | |
parent | 956ecc806cc91bd52fd27c9ecc04011b630cfbc5 (diff) |
removes unsound cases, adds unrolling
Diffstat (limited to 'test/regress/regress0/strings')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 12 | ||||
-rw-r--r-- | test/regress/regress0/strings/cardinality.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop002.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop003.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop004.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop006.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 10 |
7 files changed, 18 insertions, 25 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 699a7ff3c..2b0954cad 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,11 +26,13 @@ TESTS = \ str004.smt2 \ str005.smt2 \ model001.smt2 \ - loop001.smt2 -# loop002.smt2 \ -# loop003.smt2 \ -# loop004.smt2 \ -# loop005.smt2 \ + loop001.smt2 \ + loop002.smt2 \ + loop003.smt2 \ + loop007.smt2 + +# loop004.smt2 +# loop005.smt2 # loop006.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2 index 5c4771d71..2baac51ce 100644 --- a/test/regress/regress0/strings/cardinality.smt2 +++ b/test/regress/regress0/strings/cardinality.smt2 @@ -1,7 +1,7 @@ (set-logic ALL_SUPPORTED) (set-info :status unsat) -(set-option :str-cardinality 2) +(set-option :str-alphabet-card 2) (declare-fun x () String) (declare-fun y () String) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 index a47b959f5..2f96241dc 100644 --- a/test/regress/regress0/strings/loop002.smt2 +++ b/test/regress/regress0/strings/loop002.smt2 @@ -1,16 +1,9 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) -(declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) (assert (= (str.++ x "ba") (str.++ "ab" x))) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 index a535f7583..b4fbcf7d5 100644 --- a/test/regress/regress0/strings/loop003.smt2 +++ b/test/regress/regress0/strings/loop003.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2 index 7b39bf2d3..cc9a19a9e 100644 --- a/test/regress/regress0/strings/loop004.smt2 +++ b/test/regress/regress0/strings/loop004.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2 index 8c3690c61..cd5dd86ce 100644 --- a/test/regress/regress0/strings/loop006.smt2 +++ b/test/regress/regress0/strings/loop006.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 new file mode 100644 index 000000000..8d789edb3 --- /dev/null +++ b/test/regress/regress0/strings/loop007.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (= (str.++ x y "aa") (str.++ "aa" y x)))
+(assert (= (str.len x) 1))
+
+(check-sat)
\ No newline at end of file |