Prevent incorrect internal error message

Source/DafnyDriver/CliCompilation.cs

@@ -22,15 +22,18 @@ namespace DafnyDriver.Commands;
 public record CanVerifyResult(ICanVerify CanVerify, IReadOnlyList<VerificationTaskResult> Results);
 
 public class CliCompilation {
+  private readonly ILogger<CliCompilation> logger;
   public Compilation Compilation { get; }
   private readonly ConcurrentDictionary<MessageSource, int> errorsPerSource = new();
   private int errorCount;
   private int warningCount;
   public bool DidVerification { get; private set; }
 
   private CliCompilation(
+    ILogger<CliCompilation> logger,
     CreateCompilation createCompilation,
     DafnyOptions options) {
+    this.logger = logger;
     Options = options;
 
     if (options.DafnyProject == null) {
@@ -86,7 +89,7 @@ public static CliCompilation Create(DafnyOptions options) {
     var fileSystem = OnDiskFileSystem.Instance;
     ILoggerFactory factory = new LoggerFactory();
     var telemetryPublisher = new CliTelemetryPublisher(factory.CreateLogger<TelemetryPublisherBase>());
-    return new CliCompilation(CreateCompilation, options);
+    return new CliCompilation(factory.CreateLogger<CliCompilation>(), CreateCompilation, options);
 
     Compilation CreateCompilation(ExecutionEngine engine, CompilationInput input) =>
       new(factory.CreateLogger<Compilation>(), fileSystem,
@@ -230,24 +233,11 @@ public async IAsyncEnumerable<CanVerifyResult> 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<Task> { 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 <https://github.com/dafny-lang/dafny/issues>.\n");
-          break;
-        }
-
         await results.Finished.Task;
+        done++;
       } catch (ProverException e) {
         Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message);
         yield break;

Source/TestDafny/MultiBackendTest.cs

@@ -120,7 +120,8 @@ private async Task<int> 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<ResolutionSetting>() {
       new ResolutionSetting(
@@ -243,7 +244,7 @@ public async Task<int> 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<ResolutionSetting>() {
       new("legacy", new string[] { }, new string[] { ".expect" },
@@ -325,7 +326,7 @@ private async Task<int> 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<string> ReadAllLines(string s) {
   }
 
   private static async Task<(int, string, string)> RunDafny(IEnumerable<string> 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<string> 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();

docs/dev/news/5209.fix

@@ -0,0 +1 @@
+No longer emit an incorrect internal error while waiting for verification message

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"