I changed an assert to an assert-soft and now I get an error "unabled nested data-type expression". What does this mean?
It is a typo in the code. The optimization mode believes it can translate your data-type expressions into enumeration types, but encounters an expression it does not know to handle. The code needs to be fixed to check for this condition. A small repro would be useful. I can fix the typo in the exception message, but it will not address the bug. If you can file an issue on https://github.com/z3prover with repro it will be appreciated.