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
This is because the internal function for > dynamically checks types, and since x is completely unrestricted, the branch for it being a list is sat, but then errors as it's being compared to an int.
This should be reported as an error during lifting, but the error result is somehow lost in the interpreter, and can't be found when trying to step.
The text was updated successfully, but these errors were encountered:
This is because expression evaluation is not allowed to error in GIL, while it should.
The signature of expression evaluation is basically Store.t -> Expr.t -> Val.t, when it should be Store.t -> Expr.t -> Val.t result. In case where it fails, Gillian just crashes instead of propagating the error.
I think we fixed this before when it was a general engine problem; running this code under regular WPST works fine, it gives the expected result.
This problem seems to only pop up when debugging, so I think it's something specific to how G_Interpreter stores confs or results in this context (read: I think it's my fault 😛).
This WISL code causes an error when debugging:
This is because the internal function for
>
dynamically checks types, and sincex
is completely unrestricted, the branch for it being a list is sat, but then errors as it's being compared to an int.This should be reported as an error during lifting, but the error result is somehow lost in the interpreter, and can't be found when trying to step.
The text was updated successfully, but these errors were encountered: