From d12b62783c6681d5ef4cdc358ea55d1620b1d435 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Tue, 20 Dec 2022 15:07:45 +0100
Subject: [PATCH] Fix options for 'dafny resolve' (#3227)

Fixes https://github.com/dafny-lang/dafny/issues/3218

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 Source/DafnyCore/Options/CommonOptionBag.cs | 2 +-
 Source/DafnyCore/Options/ICommandSpec.cs    | 6 +++---
 Source/DafnyLanguageServer/ServerCommand.cs | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 66611c1cc91..d359b31c82c 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -106,7 +106,7 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
     ArgumentHelpName = "language"
   };
 
-  public static readonly Option<bool> UnicodeCharacters = new("--unicode-char",
+  public static readonly Option<bool> UnicodeCharacters = new("--unicode-char", () => false,
     @"
 false - The char type represents any UTF-16 code unit.
 true - The char type represents any Unicode scalar value.".TrimStart());
diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index 6474b232426..62f2fa0587c 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -27,10 +27,13 @@ static ICommandSpec() {
   public static Argument<IEnumerable<FileInfo>> FilesArgument { get; }
 
   public static IReadOnlyList<Option> VerificationOptions = new Option[] {
+    CommonOptionBag.RelaxDefiniteAssignment,
     BoogieOptionBag.VerificationTimeLimit,
     CommonOptionBag.VerifyIncludedFiles,
     CommonOptionBag.ManualLemmaInduction,
     CommonOptionBag.SolverPath,
+    CommonOptionBag.DisableNonLinearArithmetic,
+    BoogieOptionBag.BoogieArguments,
   }.ToList();
 
   public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
@@ -55,15 +58,12 @@ static ICommandSpec() {
     BoogieOptionBag.Cores,
     CommonOptionBag.Libraries,
     CommonOptionBag.Plugin,
-    BoogieOptionBag.BoogieArguments,
     CommonOptionBag.Prelude,
-    CommonOptionBag.RelaxDefiniteAssignment,
     Function.FunctionSyntaxOption,
     CommonOptionBag.QuantifierSyntax,
     CommonOptionBag.WarnShadowing,
     CommonOptionBag.WarnMissingConstructorParenthesis,
     PrintStmt.TrackPrintEffectsOption,
-    CommonOptionBag.DisableNonLinearArithmetic,
     CommonOptionBag.UnicodeCharacters,
   });
 
diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs
index 5d465b0cd63..c7089640bae 100644
--- a/Source/DafnyLanguageServer/ServerCommand.cs
+++ b/Source/DafnyLanguageServer/ServerCommand.cs
@@ -46,9 +46,9 @@ related locations
     GhostIndicators,
     LineVerificationStatus,
     VerifySnapshots,
-    BoogieOptionBag.VerificationTimeLimit,
     CommonOptionBag.EnforceDeterminism,
-  }.Concat(ICommandSpec.CommonOptions);
+  }.Concat(ICommandSpec.VerificationOptions).
+    Concat(ICommandSpec.CommonOptions);
 
   public Command Create() {
     var command = new Command("server", "Start the Dafny language server");