Add a few more regressions.

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 98e7e744caf3f9227c67643f6e2c2427ec324469..558d170d79921c03d4a192ef30e8232be0589cc7 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -63,7 +63,8 @@ TESTS =       \
        union-1b-flip.smt2 \
        union-1b.smt2 \
        union-2.smt2 \
-       dt-simp-mem.smt2
+       dt-simp-mem.smt2 \
+       card3-ground.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2
new file mode 100644 (file)
index 0000000..54a9a5c
--- /dev/null
+++ b/test/regress/regress0/sets/card3-ground.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun S () (Set Int))
+(assert (>= (card S) 3))
+(assert (not (member 1 S)))
+(check-sat)

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index b305b69c604b6309ca727cfd2985aaa7fe20d02a..2e4fd4e1cefb2bf2ecd37a73365b8f1b60b8ff85 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -83,7 +83,9 @@ TESTS = \
   cmu-dis-0707-3.smt2 \
   nf-ff-contains-abs.smt2  \
   csp-prefix-exp-bug.smt2 \
-  cmu-substr-rw.smt2  
+  cmu-substr-rw.smt2 \
+  gm-inc-071516-2.smt2 \
+  cmu-inc-nlpp-071516.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 b/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2
new file mode 100644 (file)
index 0000000..1208ca1
--- /dev/null
+++ b/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-fun url () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (not (= (ite (str.contains url "javascript:alert(1);") 1 0) 0))) (not (not (= (ite (= (str.len url) 0) 1 0) 0)))) (not (not (= (ite (= (str.at url 0) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\f") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\f") 1 0) 0)))) (not (= (ite (str.prefixof "javascript:alert(1);" url) 1 0) 0))))
+
+(check-sat)

diff --git a/test/regress/regress0/strings/gm-inc-071516-2.smt2 b/test/regress/regress0/strings/gm-inc-071516-2.smt2
new file mode 100644 (file)
index 0000000..1650190
--- /dev/null
+++ b/test/regress/regress0/strings/gm-inc-071516-2.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-fun value2 () String)
+(declare-fun key2 () String)
+
+(assert (and (and (and (and (and (and (not (not (= (ite (str.contains value2 "=") 1 0) 0))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (not (= (str.indexof value2 "=" 0) (- 1))) 1 0) 0))) (not (not (= (ite (str.contains value2 ",") 1 0) 0)))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (= key2 "cache-control") 1 0) 0))) (not (= (ite (= key2 "cache-control") 1 0) 0))))
+
+(check-sat)