Fixed tests

dafny-lang · Jan 31, 2025 · 4d5a51b · 4d5a51b
1 parent 6512bc3
commit 4d5a51b
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 4 deletions.
diff --git 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
@@ -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);
       }