From c63eeca9a9688c7bc9ede1c3cd0ec2396b489da7 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 25 Oct 2023 13:08:42 -0700
Subject: [PATCH] Allow text and csv loggers together (#4714)

An extraneous `return` was preventing multiple verification loggers from
running.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.
---
 .../DafnyDriver/VerificationResultLogger.cs   |  1 -
 .../LitTest/logger/MultipleLoggers.dfy        | 42 +++++++++++++++++++
 2 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/MultipleLoggers.dfy

diff --git a/Source/DafnyDriver/VerificationResultLogger.cs b/Source/DafnyDriver/VerificationResultLogger.cs
index 0d9e4e48f79..35286248ac3 100644
--- a/Source/DafnyDriver/VerificationResultLogger.cs
+++ b/Source/DafnyDriver/VerificationResultLogger.cs
@@ -65,7 +65,6 @@ public static void RaiseTestLoggerEvents(DafnyOptions options, ProofDependencyMa
           var textLogger = new TextLogger(depManager, options.OutputWriter);
           textLogger.Initialize(parameters);
           textLogger.LogResults(verificationResults);
-          return;
         } else {
           throw new ArgumentException($"unsupported verification logger config: {loggerConfig}");
         }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/MultipleLoggers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/MultipleLoggers.dfy
new file mode 100644
index 00000000000..4f265c40f11
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/MultipleLoggers.dfy
@@ -0,0 +1,42 @@
+// RUN: %exits-with 4 %baredafny verify --log-format:text --log-format:csv";"LogFileName="%t.csv" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK: Overall outcome: Errors
+// Check that the CSV file exists
+// RUN: %diff "%t.csv" "%t.csv"
+
+method ExampleWithSplits() returns (y: int)
+  ensures y >= 0
+{
+  var x: int;
+  x := 5;
+  y := 0;
+  while (x > 0)
+    invariant x + y == 5
+    invariant x*x <= 25
+  {
+    x := x - 1;
+    assert {:split_here} (x+y) * (x+y) > 25;
+    y := y + 1;
+    if (x < 3) {
+      assert 2 < 2;
+      assert {:split_here} y*y > 4;
+    }
+    else {
+      assert {:split_here} y*y*y < 8;
+      assert 2 < 2;
+    }
+    assert {:split_here} (x+y) * (x+y) == 25;
+  }
+}
+
+method ExampleWithoutSplits() {
+  assert 1 + 1 == 2;
+  assert 2 + 2 == 4;
+  assert 3 + 3 == 6;
+}
+
+method AnotherExampleWithoutSplits() {
+  assert 1 + 1 == 2;
+  assert 2 + 2 == 4;
+  assert 3 + 3 == 6;
+}