Skip to content
New issue

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 Generation) Fix #3726 bug leading to stack overflow during test generation #3727

Merged
merged 10 commits into from
May 25, 2023

Conversation

Dargones
Copy link
Collaborator

Fixes #3726

This PR fixes a situation in which test generation gets into infinite recursion when trying to construct a potentially self-referential object that the verifier gives no information about (see the test, which is also the example in the linked issue). The main problem was that existing code compared types by reference in one instance in which a comparison of the types's string representations should have been used.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

atomb
atomb previously approved these changes May 24, 2023
@atomb atomb enabled auto-merge (squash) May 24, 2023 15:24
@atomb atomb merged commit df1f683 into dafny-lang:master May 25, 2023
19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

(Test Generation) stack overflow during test generation related to self-referencing objects
2 participants