Fixed CI + enhanced error reporting

dafny-lang · Jan 24, 2025 · 54e6ec2 · 54e6ec2
1 parent 61a457f
commit 54e6ec2
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs
@@ -292,12 +292,12 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
         bool verified;
         PipelineOutcome outcome;
         IDictionary<string, PipelineStatistics> moduleStats;
+        dafnyProgram.ProofDependencyManager = depManager;
         if (!options.DafnyVerify) {
           verified = false;
           outcome = PipelineOutcome.Done;
           moduleStats = new Dictionary<string, PipelineStatistics>();
         } else {
-          dafnyProgram.ProofDependencyManager = depManager;
           var boogiePrograms =
             await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList());
 
@@ -338,7 +338,7 @@ public async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!*
         }
 
         var failBecauseOfDiagnostics = dafnyProgram.Reporter.FailCompilationMessage;
-        if (!verified) {
+        if (!verified && options.DafnyVerify) {
           exitValue = ExitValue.VERIFICATION_ERROR;
         } else if (!compiled) {
           exitValue = ExitValue.COMPILE_ERROR;

diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs
@@ -507,7 +507,7 @@ await output.WriteLineAsync(
     }
     await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:");
     await output.WriteLineAsync(outputString);
-    await output.WriteLineAsync("Error:");
+    await output.WriteLineAsync($"Error (code={exitCode}):");
     await output.WriteLineAsync(error);
     return exitCode;
   }