diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-30 14:10:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-30 14:10:27 -0500 |
| commit | 9b89eb1c0a7c2e9b5be9b9a80e9e24473454ce52 (patch) | |
| tree | c41341609ed64dbf1c096d316ca46f853ddb0a8e /test/regress/regress0/quantifiers | |
| parent | 7372eab3e013b45516f499e0096e615a124ecfd4 (diff) | |
Fix quantifiers dynamic split module for parametric datatypes (#7085)
Fixes #6838.
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/issue6838-qpdt.smt2 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 new file mode 100644 index 000000000..8aad3c708 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatype Box (par (A) ((box (unbox A))))) +(assert (forall ((xy (Box Bool))) (unbox xy))) +(check-sat) |