Q: Enum sort numerals

[wintersteiger]

We've seen a change in behaviour while trying to upgrade to a more recent version of Z3. I bisected it down to b7169e2 which changed is_numeral_ext to return true for enum-sort constructors, here:

z3/src/ast/dl_decl_plugin.cpp

Line 747 in 1b6c7d6

if (dt.is_enum_sort(c->get_sort()) && dt.is_constructor(c))

Is it intentional that this is considered a numeral, even if the user did not explicitly ask for an enum sort (but "accidentally" created one with 0-field constructors)?

[NikolajBjorner]

This change was made for aligning internal behavior for the datalog engine. The external behavior seems affected because the function for checking whether an AST is a numeral then returns true for an enumeration sort, but the function for retrieving the numeric value will fail. I have updated the API behavior.

[wintersteiger]

Awesome, many thanks!