Z3::AnySort

Any sort, as a value. The sorts with nothing to configure are singletons, and a Crystal class is already one of those, so they are the classes themselves - while a Bitvec or a Seq has to be instantiated with its size or its element sort.

Whichever it is, every sort answers to_unsafe with its Z3 sort, from_ast with an expression of itself, and cast with a Crystal object converted into one. Those three are what a Seq needs, since its element sort is only known at runtime.