- Detect definitions of ADTs that wil lbe problematic for solvers to
  handle. e.g. case class Ls(elems: List[Cons[T]])

- Use IncrementalBijections in native z3 solvers