diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-31 07:43:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-31 12:43:05 +0000 |
| commit | 1954e0a0bd07ab2236c59bee2bc3da53e2018f23 (patch) | |
| tree | ffb3734f124d236e3bd04f5750d9add912b7bc8d | |
| parent | af1b3974022509e26fc14bfe6cb49cb73074b32e (diff) | |
Make regular expression sort not closed enumerable (#7092)
This ensures we don't try to apply e.g. enumerative instantiation to quantified formulas over regular expressions, since no type enumerator exists for RE.
Fixes #6750.
| -rw-r--r-- | src/expr/type_node.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index fa6a56c99..a7747c674 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -208,7 +208,7 @@ bool TypeNode::isClosedEnumerable() if (!getAttribute(IsClosedEnumerableComputedAttr())) { bool ret = true; - if (isArray() || isSort() || isCodatatype() || isFunction()) + if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp()) { ret = false; } |