Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Counterexamples] Fix stack overflow during counterexample extraction…
… 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]>
- Loading branch information