From 6c58094be960ddca3a2187081bac769da61cc2af Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Aug 2016 12:47:54 -0500 Subject: [PATCH] Add a few more regressions. --- test/regress/regress0/sets/Makefile.am | 3 ++- test/regress/regress0/sets/card3-ground.smt2 | 6 ++++++ test/regress/regress0/strings/Makefile.am | 4 +++- test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 | 9 +++++++++ test/regress/regress0/strings/gm-inc-071516-2.smt2 | 10 ++++++++++ 5 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/sets/card3-ground.smt2 create mode 100644 test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 create mode 100644 test/regress/regress0/strings/gm-inc-071516-2.smt2 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) -- 2.30.2