removes unsound cases, adds unrolling

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