From 4d5a51b6489ba3517f42499f6d2d6587bfd892ba Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Fri, 31 Jan 2025 08:44:35 -0600
Subject: [PATCH] Fixed tests

---
 Source/DafnyCore/DafnyOptions.cs             | 15 ++++++++++++---
 Source/DafnyCore/Verifier/BoogieGenerator.cs |  2 +-
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 1ad516274e..37bcefdf77 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -73,9 +73,18 @@ public T Get<T>(Argument<T> argument) {
 
 
     public T Get<T>(Option<T> option) {
-      return (T)Options.OptionArguments.GetOrDefault(option, () => ((IValueDescriptor<T>)option) is {
-        HasDefaultValue: true
-      } valueDescriptor ? valueDescriptor.GetDefaultValue() : (object)default(T));
+      return (T)Options.OptionArguments.GetOrDefault(option, () => (object)default(T));
+    }
+
+
+    public T GetOrOptionDefault<T>(Option<T> option) {
+      return (T)Options.OptionArguments.GetOrDefault(option, () => 
+       ((IValueDescriptor<T>)option) is {
+          HasDefaultValue: true
+        } valueDescriptor
+          ? valueDescriptor.GetDefaultValue()
+          : (object)default(T)
+      );
     }
 
     public object Get(Option option) {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
index bf1a439cd9..0f98bfff7a 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -701,7 +701,7 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) {
         return new Bpl.Program();
       }
 
-      if (Options.Get(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) {
+      if (Options.GetOrOptionDefault(CommonOptionBag.LogLevelOption).CompareTo(LogEventLevel.Verbose) <= 0) {
         Options.OutputWriter.WriteLine("Starting translation to Boogie of module " + forModule.FullDafnyName);
       }