From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 12 Aug 2016 17:47:54 +0000 (-0500)
Subject: Add a few more regressions.
X-Git-Tag: cvc5-1.0.0~6040^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c58094be960ddca3a2187081bac769da61cc2af;p=cvc5.git

Add a few more regressions.
---

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 98e7e744c..558d170d7 100644
--- 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
index 000000000..54a9a5cfc
--- /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 b305b69c6..2e4fd4e1c 100644
--- 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
index 000000000..1208ca169
--- /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
index 000000000..1650190f8
--- /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)