alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Printing unknown reason

Open Halbaroth opened this issue 2 years ago • 2 comments

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.

Halbaroth avatar Sep 22 '23 13:09 Halbaroth

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.

Stevendeo avatar Nov 28 '23 13:11 Stevendeo

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...

Stevendeo avatar Nov 28 '23 14:11 Stevendeo

Works now.

bclement-ocp avatar Jul 11 '24 07:07 bclement-ocp