ToDo list Occurs check Support for converting results to S-expressions General constraints support Benchmarking, profiling and performance optimizations Parallelization support A few interesting examples