-
Notifications
You must be signed in to change notification settings - Fork 256
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
Crash using subset type #4724
Comments
Was able to reproduce the issue with 4.3.0 and nightly. |
I think the problem is that the type inference used to type [] as seq but now types [] as seq31. It makes the Boogie generator fail as it expects a sequence display expression to have a collection type and not a user defined type. |
Found the source of the issue. PR #4538 modified AST/Expressions/DefaultValueExpression.cs and added this.ResolvedExpression.Type = this.Type; to the method FillIn. Commenting out that line fixes this issue. |
### Description Fix for issue #4724 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Dafny version
nightly
Code to produce this issue
Command to run and resulting output
What happened?
This code was working in Dafny 4.2.0 but crashes now in latest nightly.
What type of operating system are you experiencing the problem on?
Windows
The text was updated successfully, but these errors were encountered: