From 1954e0a0bd07ab2236c59bee2bc3da53e2018f23 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 31 Aug 2021 07:43:05 -0500 Subject: [PATCH] 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. --- src/expr/type_node.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; } -- 2.30.2