diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-30 23:29:57 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-30 23:29:57 -0500 |
commit | a747f01c1ee737bb8c4c1cc8ce355b79078d03d7 (patch) | |
tree | 49351b3e775cde995808de15d106f415770a9d12 /test/regress/regress0 | |
parent | cf4dd7abde3554156ff26684e189c1de40f51b9b (diff) |
replace with a new method for disequality, move to QF_S
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop001.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop002.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop003.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop005.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/strings/model001.smt2 | 2 |
7 files changed, 9 insertions, 14 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index a1ae66a5f..90872cf4d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,14 +27,13 @@ TESTS = \ str005.smt2 \ model001.smt2 \ loop001.smt2 \ + loop002.smt2 \ loop003.smt2 \ + loop004.smt2 \ + loop005.smt2 \ + loop006.smt2 \ loop007.smt2 -# loop002.smt2 -# loop004.smt2 -# loop005.smt2 -# loop006.smt2 - FAILING_TESTS = EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/strings/loop001.smt2 b/test/regress/regress0/strings/loop001.smt2 index 11460b335..815acce5c 100644 --- a/test/regress/regress0/strings/loop001.smt2 +++ b/test/regress/regress0/strings/loop001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 index 2f96241dc..90492189f 100644 --- a/test/regress/regress0/strings/loop002.smt2 +++ b/test/regress/regress0/strings/loop002.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 index b4fbcf7d5..1247170c9 100644 --- a/test/regress/regress0/strings/loop003.smt2 +++ b/test/regress/regress0/strings/loop003.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 6e5fc96d4..4401ef794 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -1,7 +1,3 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -; EXIT: 10 -; (set-logic QF_S) (set-info :status sat) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index 0534d8b53..bea4037d1 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (declare-fun x () String) diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2 index 2832b5c96..ac43afee1 100644 --- a/test/regress/regress0/strings/model001.smt2 +++ b/test/regress/regress0/strings/model001.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic QF_S) (set-info :status sat) (set-option :produce-models true) |