[agnishom]

Thanks. Yes, there are comparisons with Z3 towards the end of the post.

I don't think expressiveness applies here.