search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

Fatal Error when step limit reached #1244

Open claudemarche opened 1 month ago

claudemarche commented 1 month ago

When Alt-Ergo reaches the given step bound, an uncaught exception is signaled. It is desirable to display a proper information message and not an error message, this is a perfectly expected potential answer. For example, a SMTLIB-style message

unknown (RESOURCEOUT)

would be perfect. Moreover: we want the prover to continue, and answer to the next query, that could be for example

(get-model)

and get a potential model. I attach a reproducer. Here is the output I get with Alt-Ergo 2.6.0:

$ alt-ergo --steps-bound=10 ae-fatal-error-step-limit.psmt2
Fatal error: exception AltErgoLib.Util.Step_limit_reached(10)
claudemarche commented 1 month ago

I would like to put a label "Décysif" on such an issue. Why am I not allowed to put labels on issues?

bclement-ocp commented 1 month ago

This should have been fixed in #936 but seems we re-introduced the issue.

I am not sure why you can't add labels; I think this needs you to have the "Triage" permission but it does not appear in the list of possible permissions… I gave you "Read" access to the repo in case it would allow me to upgrade to "Triage" but that does not seem possible either. I have added the "decysif" label for this one.

claudemarche commented 1 month ago

I still can't modify labels. Never mind, it is not important.

bclement-ocp commented 1 month ago

Turns out the fix in #936 only applies if the step limit is reached while processing an assertion, not while processing (check-sat).

Moreover: we want the prover to continue, and answer to the next query, that could be for example

The current semantics of the step limit is that it is a global limit; we only support a per-goal time limit, so any further queries would immediately return unknown as well. We also are currently not able to provide a model after the step limit is reached because the required internal state is thrown away (the step limit is internally implemented as an exception).

The steps limit mechanism was designed when Alt-Ergo supported neither incremental queries nor model generation, and it seems clear that the implementation is no longer satisfactory. I have a fix ( #1245 ) to avoid returning a fatal error; fixing the rest of the issue w.r.t incrementality and model generation after a timeout will require more work.