We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[] > test [] > parent [self x] > f x.sub 5 > t seq > @ assert (0.less t) x [self y1] > g self.f self y1 > @ [self y2] > gg self.g self y2 > @ [self y3] > ggg self.gg self y3 > @ [self z] > h z > @ [] > child test.parent > @ [self y] > f y > @ [self z] > h self.ggg self z > @
RESULT BY AnOdin: [Unjustified Assumption] Method g is not referentially transparent
RESULT BY AnOdin: Odin is not able to analyze the code, due to: Symbol value-of-before-f not declared
I suppose that it is somehow related to a length of a calls chain.(not confirmed based on #36) With shortened chain, it works well.
[] > test [] > parent [self x] > f x.sub 5 > t seq > @ assert (0.less t) x [self y1] > g self.f self y1 > @ [self y2] > gg self.g self y2 > @ [self z] > h z > @ [] > child test.parent > @ [self y] > f y > @ [self z] > h self.gg self z > @
The text was updated successfully, but these errors were encountered:
@Leosimetti as discussed, we need to use define-funs-rec to enable (mutually) recursive definitions of function values and function properties.
define-funs-rec
Sorry, something went wrong.
Leosimetti
Successfully merging a pull request may close this issue.
Problematic code
Expected result
Actual result
Assumption
I suppose that it is somehow related to a length of a calls chain.(not confirmed based on #36) With shortened chain, it works well.Code
Results
The text was updated successfully, but these errors were encountered: