Fatal failure in StringEnumerator::StringEnumerator() at src/theory/strings/type_enumerator.cpp:260

[aniemetz]

cvc5/cvc5@ccdd564ea murxla/murxla@eacdc9c

(set-logic ALL)
(set-option :produce-models true)
(declare-datatype x ((_x (x8 RegLan))))
(declare-const x x)
(declare-fun _x (x) Float16)
(check-sat)
(get-value ((fp.leq (_x x) (_x x))))

error:

Fatal failure within cvc5::theory::strings::StringEnumerator::StringEnumerator(cvc5::TypeNode, cvc5::theory::TypeEnumeratorProperties*) at src/theory/strings/type_enumerator.cpp:260
Check failure

 type.getKind() == kind::TYPE_CONSTANT && type.getConst<TypeConstant>() == STRING_TYPE

[ajreynol]

We should disallow regular languages as fields to datatypes.