diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-20 18:23:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 18:23:40 -0700 |
| commit | 578cda677d0cc62991f3ab38d0bc26074c8c28d6 (patch) | |
| tree | a231ffb813653c1e2da5b38f24a9bd87a6f16b45 /test/regress/regress1/strings | |
| parent | 2f903dcfff1eded7a75f71eede947719b72513d9 (diff) | |
| parent | e590612dc4421d45cacc451a7b8a162acd9c7943 (diff) | |
Merge branch 'master' into fix1649fix1649
Diffstat (limited to 'test/regress/regress1/strings')
4 files changed, 51 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2 new file mode 100644 index 000000000..6673dc3b9 --- /dev/null +++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(set-option :check-unsat-cores true) +(declare-fun i8 () Int) +(declare-fun st6 () (Set String)) +(declare-fun st8 () (Set String)) +(declare-fun str6 () String) +(declare-fun str7 () String) +(assert (= 0 (card st8))) +(assert (str.in_re str6 (re.opt re.none))) +(assert (str.in_re (str.substr str7 0 i8) re.allchar)) +(assert (xor true (subset st8 st6) (not (= str7 str6)) true)) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-3-seq.smt2 b/test/regress/regress1/strings/issue6653-3-seq.smt2 new file mode 100644 index 000000000..a48fc7664 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-3-seq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(declare-fun z () Int) +(declare-fun a () (Seq Int)) +(assert (not (= (seq.nth a 1) (seq.nth a z)))) +(assert (= z (- 1))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat) diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2 new file mode 100644 index 000000000..93a4985d4 --- /dev/null +++ b/test/regress/regress1/strings/seq-cardinality.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Seq (_ BitVec 1))) +(declare-fun y () (Seq (_ BitVec 1))) +(declare-fun z () (Seq (_ BitVec 1))) + +(assert (= (seq.len x) 1)) +(assert (= (seq.len y) 1)) +(assert (= (seq.len z) 1)) +(assert (distinct x y z)) +(check-sat) |