diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 10f96cb01ae..e4950514827 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -26,7 +26,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest { public class DafnyLanguageServerTestBase : LanguageProtocolTestBase { protected readonly string SlowToVerify = @" -lemma {:timeLimit 1} SquareRoot2NotRational(p: nat, q: nat) +lemma {:rlimit 100} SquareRoot2NotRational(p: nat, q: nat) requires p > 0 && q > 0 ensures (p * p) != 2 * (q * q) { diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 4297154ce18..80f92dfdbe4 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -90,8 +90,8 @@ public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() { var documentItem = CreateTestDocument(SlowToVerify, "DiagnosticsForVerificationTimeout.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); - Assert.Contains("timed out", diagnostics[0].Message); - Assert.Equal(new Range(0, 21, 0, 43), diagnostics[0].Range); + Assert.Contains("Verification out of resource", diagnostics[0].Message); + Assert.Equal(new Range(0, 20, 0, 42), diagnostics[0].Range); } [Fact] diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 37aab2cfce0..1400b2f3a47 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -367,7 +367,7 @@ await SetUp(options => { var successfulRun = await client.RunSymbolVerification(new TextDocumentIdentifier(documentItem.Uri), methodHeader, CancellationToken); Assert.True(successfulRun); - var range = new Range(0, 21, 0, 43); + var range = new Range(0, 20, 0, 42); await WaitForStatus(range, PublishedVerificationStatus.Running, CancellationToken); await WaitForStatus(range, PublishedVerificationStatus.Error, CancellationToken);