diff options
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) |