You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, when Alt-Ergo reaches the steps limit given using --steps-bound, the reporting is weird, e.g.:
[Error]; Fatal Error: Steps limit reached: 10
There is no reason for considering the reaching of the steps limit as a "fatal error" or even an error. It should instead report a regular unknown or I don't know result, as it does when the time limit is reached
Moreover, it would be better to comply to the more or less SMT compliant answer, where one gets extra information using (get-info :reason-unknown)
The text was updated successfully, but these errors were encountered:
We have added support for (get-info :reason-unknown) in #853 which will be part of the next release.
However it looks like we still treat the steps limit as an error (although it is now in stm2 format, which is an improvement I guess), so that part still needs to be fixed (we should treat steps limit like a timeout, it shouldn't be part of the Errors module):
Currently, when Alt-Ergo reaches the steps limit given using
--steps-bound
, the reporting is weird, e.g.:There is no reason for considering the reaching of the steps limit as a "fatal error" or even an error. It should instead report a regular
unknown
orI don't know
result, as it does when the time limit is reachedMoreover, it would be better to comply to the more or less SMT compliant answer, where one gets extra information using
(get-info :reason-unknown)
The text was updated successfully, but these errors were encountered: