Merge branch 'master' of github.com:tiliang/CVC4

14 files changed, 43 insertions, 35 deletions

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 269ec49ed..a1ae66a5f 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -25,11 +25,14 @@ TESTS =	\
   str003.smt2 \
   str004.smt2 \
   str005.smt2 \
-  loop001.smt2
-# loop002.smt2 \
-# loop003.smt2 \
-# loop004.smt2 \
-# loop005.smt2 \
+  model001.smt2 \
+  loop001.smt2 \
+  loop003.smt2 \
+  loop007.smt2
+
+# loop002.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..465ea0b5e 100644
--- a/test/regress/regress0/strings/cardinality.smt2
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -1,7 +1,7 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (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..8d2ff8096 100644
--- a/test/regress/regress0/strings/loop004.smt2
+++ b/test/regress/regress0/strings/loop004.smt2
@@ -1,8 +1,4 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
-(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 ec294b9bb..6e5fc96d4 100644
--- a/test/regress/regress0/strings/loop005.smt2
+++ b/test/regress/regress0/strings/loop005.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 ; EXIT: 10
 ;
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2
index 8c3690c61..288a5f60c 100644
--- a/test/regress/regress0/strings/loop006.smt2
+++ b/test/regress/regress0/strings/loop006.smt2
@@ -1,8 +1,4 @@
-; COMMAND-LINE: --no-check-models
-; EXPECT: sat
-; EXIT: 10
-;
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status sat)
 
 (declare-fun x () String)
@@ -12,6 +8,8 @@
 (declare-fun w1 () String)
 (declare-fun w2 () String)
 
-(assert (= (str.++ x y z) (str.++ x z y)))
+;(assert (= (str.++ x y) (str.++ y x)))
+
+(assert (not (= (str.++ x y) (str.++ y x))))
 
 (check-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
diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2
new file mode 100644
index 000000000..e4e35f40d
--- /dev/null
+++ b/test/regress/regress0/strings/model001.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)

+(set-info :status sat)

+(set-option :produce-models true)

+

+(declare-fun x () String)

+(declare-fun y () String)

+

+(assert (not (= x y)))

+(assert (= (str.len x) (str.len y)))

+

+(check-sat)

+;(get-model)

diff --git a/test/regress/regress0/strings/str001.smt2 b/test/regress/regress0/strings/str001.smt2
index 8ae10edbe..bb2b701d8 100644
--- a/test/regress/regress0/strings/str001.smt2
+++ b/test/regress/regress0/strings/str001.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str002.smt2 b/test/regress/regress0/strings/str002.smt2
index 98b3e1e00..62512ef79 100644
--- a/test/regress/regress0/strings/str002.smt2
+++ b/test/regress/regress0/strings/str002.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str003.smt2 b/test/regress/regress0/strings/str003.smt2
index c88e1233e..0ced7f447 100644
--- a/test/regress/regress0/strings/str003.smt2
+++ b/test/regress/regress0/strings/str003.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2
index d4763adee..8a03f4481 100644
--- a/test/regress/regress0/strings/str004.smt2
+++ b/test/regress/regress0/strings/str004.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/str005.smt2 b/test/regress/regress0/strings/str005.smt2
index 4916b1df4..84cb5af01 100644
--- a/test/regress/regress0/strings/str005.smt2
+++ b/test/regress/regress0/strings/str005.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_S)
 (set-info :status unsat)
 
 (declare-fun xx () String)