diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs index 6afcacefa3b..77dd63d0695 100644 --- a/Source/DafnyDriver/CliCompilation.cs +++ b/Source/DafnyDriver/CliCompilation.cs @@ -230,24 +230,11 @@ public async IAsyncEnumerable VerifyAllLazily(int? randomSeed) foreach (var canVerify in orderedCanVerifies) { var results = canVerifyResults[canVerify]; try { - var timeLimitSeconds = TimeSpan.FromSeconds(Options.Get(BoogieOptionBag.VerificationTimeLimit)); - var tasks = new List { results.Finished.Task }; - if (timeLimitSeconds.Seconds != 0) { - tasks.Add(Task.Delay(timeLimitSeconds)); - } - if (Options.Get(CommonOptionBag.ProgressOption)) { await Options.OutputWriter.WriteLineAsync($"Verified {done}/{orderedCanVerifies.Count} symbols. Waiting for {canVerify.FullDafnyName} to verify."); } - await Task.WhenAny(tasks); - done++; - if (!results.Finished.Task.IsCompleted) { - Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok, - "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at .\n"); - break; - } - await results.Finished.Task; + done++; } catch (ProverException e) { Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message); yield break; diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs index ecc618b7c98..3741df1f1b6 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/Source/TestDafny/MultiBackendTest.cs @@ -120,7 +120,8 @@ private async Task ForEachCompiler(ForEachCompilerOptions options) { $"--print:{tmpDPrint}", options.OtherArgs.Any(option => option.StartsWith("--print")) ? "" : $"--rprint:{tmpRPrint}", $"--bprint:{tmpPrint}" - }.Concat(options.OtherArgs.Where(OptionAppliesToVerifyCommand)).ToArray(); + }.Concat(DafnyCliTests.NewDefaultArgumentsForTesting). + Concat(options.OtherArgs.Where(OptionAppliesToVerifyCommand)).ToArray(); var resolutionOptions = new List() { new ResolutionSetting( @@ -243,7 +244,7 @@ public async Task ForEachResolver(ForEachResolverOptions options) { $"--print:{tmpDPrint}", options.OtherArgs.Any(option => option.StartsWith("--print")) ? "" : $"--rprint:{tmpRPrint}", $"--bprint:{tmpPrint}" - }.Concat(options.OtherArgs.Where(OptionAppliesToVerifyCommand)).ToArray(); + }.Concat(DafnyCliTests.NewDefaultArgumentsForTesting).Concat(options.OtherArgs.Where(OptionAppliesToVerifyCommand)).ToArray(); var resolutionOptions = new List() { new("legacy", new string[] { }, new string[] { ".expect" }, @@ -325,7 +326,7 @@ private async Task RunWithCompiler(ForEachCompilerOptions options, IExecuta $"--target:{backend.TargetId}", $"--build:{tempOutputDirectory}", options.TestFile!, - }.Concat(options.OtherArgs); + }.Concat(DafnyCliTests.NewDefaultArgumentsForTesting).Concat(options.OtherArgs); if (!includeRuntime) { // We have to provide the path to DafnyRuntime.dll manually, since the program will be run // in the directory containing the DLL built from Dafny code, not the Dafny distribution. @@ -390,10 +391,9 @@ public static IList ReadAllLines(string s) { } private static async Task<(int, string, string)> RunDafny(IEnumerable arguments) { - var argumentsWithDefaults = arguments.Concat(DafnyCliTests.NewDefaultArgumentsForTesting); var outputWriter = new StringWriter(); var errorWriter = new StringWriter(); - var exitCode = await DafnyBackwardsCompatibleCli.MainWithWriters(outputWriter, errorWriter, TextReader.Null, argumentsWithDefaults.ToArray()); + var exitCode = await DafnyBackwardsCompatibleCli.MainWithWriters(outputWriter, errorWriter, TextReader.Null, arguments.ToArray()); var outputString = outputWriter.ToString(); var error = errorWriter.ToString(); return (exitCode, outputString, error); @@ -404,8 +404,7 @@ public static IList ReadAllLines(string s) { return await RunDafny(arguments); } - var argumentsWithDefaults = arguments.Concat(DafnyCliTests.NewDefaultArgumentsForTesting); - ILitCommand command = new ShellLitCommand(dafnyCliPath, argumentsWithDefaults, DafnyCliTests.ReferencedEnvironmentVariables); + ILitCommand command = new ShellLitCommand(dafnyCliPath, arguments, DafnyCliTests.ReferencedEnvironmentVariables); var outputWriter = new StringWriter(); var errorWriter = new StringWriter(); diff --git a/docs/dev/news/5209.fix b/docs/dev/news/5209.fix new file mode 100644 index 00000000000..0ed141d88c4 --- /dev/null +++ b/docs/dev/news/5209.fix @@ -0,0 +1 @@ +No longer emit an incorrect internal error while waiting for verification message \ No newline at end of file diff --git a/docs/dev/news/5295.fix b/docs/dev/news/5295.fix new file mode 100644 index 00000000000..410408824ca --- /dev/null +++ b/docs/dev/news/5295.fix @@ -0,0 +1 @@ +Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" \ No newline at end of file