Counterexample generation fails: integer overflow

[sorawee]

Version 3.7.0 (Dafny VSCode extension version 2.5.0)

Consider:

ghost const NAT_MAX := 0x7fff_ffff
ghost const NAT64_MAX := 0x7fff_ffff_ffff_ffff

newtype nat32 = x | 0 <= x <= NAT_MAX
newtype nat64 = x | 0 <= x <= NAT64_MAX

function method plus(a: nat32, b: nat32): nat32 {
    var al := a as nat64;
    var bl := b as nat64;
    a + b
}

The counterexample generation errors with:

CounterExample request failed: Error: Internal Error - System.OverflowException: Value was either too large or too small for an Int32.
   at System.Number.ThrowOverflowOrFormatException(ParsingStatus status, TypeCode type)
   at Microsoft.Boogie.Model.Number.AsInt()
   at DafnyServer.CounterexampleGeneration.DafnyModel.RegisterReservedInts() in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs:line 191
   at DafnyServer.CounterexampleGeneration.DafnyModel..ctor(Model model) in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs:line 93
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetLanguageSpecificModel(Model model) in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs:line 79
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.<GetLanguageSpecificModels>b__8_0(Counterexample c) in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs:line 75
   at System.Linq.Enumerable.SelectArrayIterator`2.MoveNext()
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.MoveNext()
   at Microsoft.Dafny.LanguageServer.LinqExtensions.WithCancellation[TEntry](IEnumerable`1 entries, CancellationToken cancellationToken)+MoveNext() in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyLanguageServer/LinqExtensions.cs:line 19
   at System.Collections.Generic.LargeArrayBuilder`1.AddRange(IEnumerable`1 items)
   at System.Collections.Generic.EnumerableHelpers.ToArray[T](IEnumerable`1 source)
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.CounterExampleLoader.GetCounterExamples() in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs:line 67
   at Microsoft.Dafny.LanguageServer.Handlers.Custom.DafnyCounterExampleHandler.Handle(CounterExampleParams request, CancellationToken cancellationToken) in /Users/soraweep/.vscode/extensions/dafny-lang.ide-vscode-2.5.0/out/resources/3.7.0/custom/arm64/dafny/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs:line 29
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
   at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<<RouteRequest>b__5>d.MoveNext()

CC: @Dargones

[Dargones]

Thank you, @sorawee! I am aware of this and have a fix here that would prevent the server from crashing. Incidentally, would it be possible to merge #2269? I have been planning a code quality improvement PR for counterexamples (including the overflow fix) and it clashes with this earlier PR since I had to change a few things in test generation as well. #2269 has been approved by @atomb but perhaps the policy is to have more than one approval? @robin-aws, could you take a look?