Haha, I've often wondered how one could answer to the wrong thread on HN, and there I am :)

Was intended for https://news.ycombinator.com/item?id=47025885

And z4 is, of course z3 (no I don't have special access to next-gen version of z3)