replace with a new method for disequality, move to QF_S

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)