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

Runtime implementation of multisets has a cardinality limit #4012

Closed
fabiomadge opened this issue May 15, 2023 · 2 comments · Fixed by #4014
Closed

Runtime implementation of multisets has a cardinality limit #4012

fabiomadge opened this issue May 15, 2023 · 2 comments · Fixed by #4014
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@fabiomadge
Copy link
Collaborator

fabiomadge commented May 15, 2023

Split off from #3988.

Dafny version

4.1.0

Code to produce this issue

method Main() {
    var x: multiset<int> := multiset{};
    x := x[1 := 18446744073709551616];
    print |x|;
}

What happened?

Crash

What type of operating system are you experiencing the problem on?

Mac

@fabiomadge fabiomadge added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: python Dafny's Python transpiler and its runtime labels May 15, 2023
@stefan-aws
Copy link
Collaborator

Can confirm the following error on my Mac with 4.1.0:

Error: Execution resulted in exception: Exception has been thrown by the target of an invocation.
System.OverflowException: Value was either too large or too small for an Int32.
   at System.Numerics.BigInteger.op_Explicit(BigInteger value)
   at Dafny.MultiSet`1.get_Count()
   at _module.__default._Main(ISequence`1 __noArgsParameter)
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)

@fabiomadge
Copy link
Collaborator Author

What about the fix?

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 lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants