alt-ergo
alt-ergo copied to clipboard
Printing unknown reason
We should support the SMT-LIB syntax (get-info :reason-unknown) to be able to print the reason why Alt-Ergo answers timeout.
See https://github.com/OCamlPro/alt-ergo/pull/829#discussion_r1332945479
The PR #837 partially solves this issue.
I have been testing something before closing this issue, and something annoying happens.
- If we set a global timeout, we stop right after the timeout so the get-info :reason-unknown is not reached
- If we set a timeout per goal and return unknown,
(get-info :reason-unknown)returns an error.
Ah, actually with the latest next (after Fix timeout) it is worse with timelimit-per-goal. As the assertion fails, it returns a first unknown before reaching check-sat which also returns unknown...
Works now.