diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-19 18:01:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-19 18:01:11 -0500 |
| commit | bda77d20d51b0ebdd8dec4bd50c6ce5faef7f218 (patch) | |
| tree | 8a814346774eea7f3b4a8af27ef0a8eb5177126b /test | |
| parent | 8fe459b1fb3843ebdbda86f24a414c46b986aa90 (diff) | |
Support sequences of fixed finite cardinality (#7371)
The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/seq-cardinality.smt2 | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 84f0ef408..a0f6f7999 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2268,6 +2268,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-cardinality.smt2 regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 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) |