projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af1b397) | patch
Make regular expression sort not closed enumerable (#7092)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 31 Aug 2021 12:43:05 +0000 (07:43 -0500)
committerGitHub <noreply@github.com>
Tue, 31 Aug 2021 12:43:05 +0000 (12:43 +0000)
commit1954e0a0bd07ab2236c59bee2bc3da53e2018f23
treeffb3734f124d236e3bd04f5750d9add912b7bc8dtree
parentaf1b3974022509e26fc14bfe6cb49cb73074b32ecommit | 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.
src/expr/type_node.cpp diff | blob | history