4 ms·
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
by poizan42 12y ago
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 12y agoThe very first example on Github show that checking a conjecture results in one of 3 outcomes: - Unsatisfied (unsat) - Satisified (sat) - Unknown (unknown)
- darkmighty 12y agoHe just stated non-termination is not an option, therefore...