Results 2 comments of Denghang

I have try to use z3 and cvc4 to solve this instance. And they will generate them all. May be we can support this feature?