[poizan42]

Uhm you can throw diophantine equations after Z3 which certainly isn't a decideable problem. I have no idea whether it errs on the side of termination (i.e. not giving an answer) or non-termination (i.e. running forever).

[deckar01]

The very first example on Github show that checking a conjecture results in one of 3 outcomes:

- Unsatisfied (unsat)

- Satisified (sat)

- Unknown (unknown)

[darkmighty]

He just stated non-termination is not an option, therefore...