-
Notifications
You must be signed in to change notification settings - Fork 254
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
Stack Overflow during Counterexample Generation #4391
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: counterexamples
Counterexample generation
Comments
atomb
pushed a commit
that referenced
this issue
Aug 9, 2023
… for some programs (#4392) Fixes #4391 This PR fixes a potential case of an infinite recursion in Dafny counterexample extraction (exemplified by the added test). The solution is to change the order in which Dafny looks at functions in the counterexample model when trying to deduce the type of a variable. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
keyboardDrummer
pushed a commit
to keyboardDrummer/dafny
that referenced
this issue
Sep 15, 2023
… for some programs (dafny-lang#4392) Fixes dafny-lang#4391 This PR fixes a potential case of an infinite recursion in Dafny counterexample extraction (exemplified by the added test). The solution is to change the order in which Dafny looks at functions in the counterexample model when trying to deduce the type of a variable. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
keyboardDrummer
pushed a commit
that referenced
this issue
Sep 19, 2023
… for some programs (#4392) Fixes #4391 This PR fixes a potential case of an infinite recursion in Dafny counterexample extraction (exemplified by the added test). The solution is to change the order in which Dafny looks at functions in the counterexample model when trying to deduce the type of a variable. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
part: counterexamples
Counterexample generation
Dafny version
nightly-2023-08-04
Code to produce this issue
Command to run and resulting output
What happened?
Stack Overflow (at Microsoft.Dafny.LanguageServer.CounterExampleGeneration.DafnyModel.GetDafnyType(Uninterpreted))
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: