From 1be23887353ae0771bd0bb287097b5a78e655952 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 16 Nov 2023 04:30:18 -0800
Subject: [PATCH 01/13] Counterexample parity for extension vs command line

---
 Source/DafnyCore/DafnyConsolePrinter.cs       |  5 ++-
 Source/DafnyCore/DafnyOptions.cs              | 13 ++++--
 Source/DafnyCore/Options/CommonOptionBag.cs   | 15 ++++++-
 Source/DafnyCore/Options/DafnyCommands.cs     |  3 +-
 Source/DafnyDriver/CompilerDriver.cs          | 40 +++++++++++--------
 Source/DafnyLanguageServer/LanguageServer.cs  |  7 ----
 .../ProgramModification.cs                    | 19 ---------
 .../server/counterexample_commandline.dfy     |  2 +-
 .../counterexample_commandline.dfy.expect     | 21 +---------
 9 files changed, 53 insertions(+), 72 deletions(-)

diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs
index 87744bb3028..64da91b90a6 100644
--- a/Source/DafnyCore/DafnyConsolePrinter.cs
+++ b/Source/DafnyCore/DafnyConsolePrinter.cs
@@ -35,13 +35,14 @@ public record VerificationResultLogEntry(
     ConditionGeneration.Outcome Outcome,
     TimeSpan RunTime,
     int ResourceCount,
-    List<VCResultLogEntry> VCResults);
+    List<VCResultLogEntry> VCResults,
+    List<Counterexample> Counterexamples);
   public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);
 
   public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) {
     return new VerificationResultLogEntry(
       verificationResult.Outcome, verificationResult.End - verificationResult.Start,
-      verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList());
+      verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
   }
 
   private static VCResultLogEntry DistillVCResult(VCResult r) {
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 9e273019b37..49d0d04205b 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -729,6 +729,7 @@ public enum IncludesModes {
 
         case "extractCounterexample":
           ExtractCounterexample = true;
+          EnhancedErrorMessages = 1;
           return true;
 
         case "verificationLogger":
@@ -1148,6 +1149,13 @@ public enum IncludesModes {
       SetZ3Option("type_check", "true");
       SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering
       SetZ3Option("smt.delay_units", "true");
+      SetZ3Option("model_evaluator.completion", "true");
+      SetZ3Option("model.completion", "true");
+      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
+        SetZ3Option("model_compress", "false");
+      } else {
+        SetZ3Option("model.compact", "false");
+      }
 
       // This option helps avoid "time travelling triggers".
       // See: https://github.com/dafny-lang/dafny/discussions/3362
@@ -1419,10 +1427,7 @@ the program.
 
 /extractCounterexample
     If verification fails, report a detailed counterexample for the
-    first failing assertion. Requires specifying the /mv:<file> option as well
-    as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
-    /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
-    /proverOpt:O:model.completion=true.
+    first failing assertion (experimental).
 
 ---- Compilation options ---------------------------------------------------
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 3f23b1a1dc5..2428d5dbe3e 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -291,6 +291,11 @@ public enum DefaultFunctionOpacityOptions {
 Not compatible with the --unicode-char:false option.
 ");
 
+  public static readonly Option<bool> ExtractCounterexample = new("--extract-counterexample", () => false,
+    @"
+If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) {
+  };
+
   static CommonOptionBag() {
     DafnyOptions.RegisterLegacyUi(Target, DafnyOptions.ParseString, "Compilation options", "compileTarget", @"
 cs (default) - Compile to .NET via C#.
@@ -475,6 +480,11 @@ public enum DefaultFunctionOpacityOptions {
         }
       });
 
+    DafnyOptions.RegisterLegacyBinding(ExtractCounterexample, (options, value) => {
+      options.ExtractCounterexample = value;
+      options.EnhancedErrorMessages = 1;
+    });
+
     DooFile.RegisterLibraryChecks(
       new Dictionary<Option, DooFile.OptionCheck>() {
         { UnicodeCharacters, DooFile.CheckOptionMatches },
@@ -522,8 +532,9 @@ public enum DefaultFunctionOpacityOptions {
       OptimizeErasableDatatypeWrapper,
       AddCompileSuffix,
       SystemModule,
-      ExecutionCoverageReport
-    );
+      ExecutionCoverageReport,
+      ExtractCounterexample
+      );
   }
 
   public static readonly Option<bool> FormatPrint = new("--print",
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 28edb04304f..865537e26e2 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -43,7 +43,8 @@ public static class DafnyCommands {
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
     CommonOptionBag.NoTimeStampForCoverageReport,
-    CommonOptionBag.VerificationCoverageReport
+    CommonOptionBag.VerificationCoverageReport,
+    CommonOptionBag.ExtractCounterexample
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index ac06e8fea31..d97544d7fa9 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -27,6 +27,7 @@
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer.CounterExampleGeneration;
 using Microsoft.Dafny.Plugins;
+using VC;
 
 namespace Microsoft.Dafny {
 
@@ -57,12 +58,6 @@ public class CompilerDriver : IDisposable {
         return (int)getFilesExitCode;
       }
 
-      if (options.ExtractCounterexample && options.ModelViewFile == null) {
-        options.Printer.ErrorWriteLine(options.OutputWriter,
-          "*** Error: ModelView file must be specified when attempting counterexample extraction");
-        return (int)ExitValue.PREPROCESSING_ERROR;
-      }
-
       using var driver = new CompilerDriver(options);
       ProofDependencyManager depManager = new();
       var exitValue = await driver.ProcessFilesAsync(dafnyFiles, otherFiles.AsReadOnly(), options, depManager);
@@ -187,7 +182,7 @@ public class CompilerDriver : IDisposable {
         Util.PrintFunctionCallGraph(dafnyProgram);
       }
       if (dafnyProgram != null && options.ExtractCounterexample && exitValue == ExitValue.VERIFICATION_ERROR) {
-        PrintCounterexample(options, options.ModelViewFile);
+        PrintCounterexample(options);
       }
       return exitValue;
     }
@@ -196,17 +191,28 @@ public class CompilerDriver : IDisposable {
     /// Extract the counterexample corresponding to the first failing
     /// assertion and print it to the console
     /// </summary>
-    private static void PrintCounterexample(DafnyOptions options, string modelViewFile) {
-      var model = DafnyModel.ExtractModel(options, File.ReadAllText(modelViewFile));
+    private static void PrintCounterexample(DafnyOptions options) {
+      var firstCounterexample = (options.Printer as DafnyConsolePrinter).VerificationResults
+        .Select(result => result.Result)
+        .Where(result => result.Outcome == ConditionGeneration.Outcome.Errors)
+        .Select(result => result.Counterexamples)
+        .Where(counterexampleList => counterexampleList != null)
+        .Select(counterexampleList => counterexampleList.FirstOrDefault(counterexample => counterexample.Model != null))
+        .FirstOrDefault(counterexample => counterexample != null);
+      if (firstCounterexample == null) {
+        return;
+      }
+      var model = new DafnyModel(firstCounterexample.Model, options);
+      var initialState = model.States.FirstOrDefault(state => state.IsInitialState);
+      if (initialState == null) {
+        return;
+      }
       options.OutputWriter.WriteLine("Counterexample for first failing assertion: ");
-      foreach (var state in model.States.Where(state => !state.IsInitialState)) {
-        options.OutputWriter.WriteLine(state.FullStateName + ":");
-        var vars = state.ExpandedVariableSet(-1);
-        foreach (var variable in vars) {
-          options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +
-                                   $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
-                                   $"{variable.Value}");
-        }
+      var vars = initialState.ExpandedVariableSet(-1);
+      foreach (var variable in vars) {
+        options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +
+                                       $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
+                                       $"{variable.Value}");
       }
     }
 
diff --git a/Source/DafnyLanguageServer/LanguageServer.cs b/Source/DafnyLanguageServer/LanguageServer.cs
index 73bbe302c99..eccb2200038 100644
--- a/Source/DafnyLanguageServer/LanguageServer.cs
+++ b/Source/DafnyLanguageServer/LanguageServer.cs
@@ -54,13 +54,6 @@ related locations
       //      A dash means write to the textwriter instead of a file.
       // https://github.com/boogie-org/boogie/blob/b03dd2e4d5170757006eef94cbb07739ba50dddb/Source/VCGeneration/Couterexample.cs#L217
       dafnyOptions.ModelViewFile = "-";
-
-      dafnyOptions.ProverOptions.AddRange(new List<string>()
-      {
-        "O:model_compress=false", // Replaced by "O:model.compact=false" if z3's version is > 4.8.6
-        "O:model.completion=true",
-        "O:model_evaluator.completion=true"
-      });
     }
 
     public static async Task Start(DafnyOptions dafnyOptions) {
diff --git a/Source/DafnyTestGeneration/ProgramModification.cs b/Source/DafnyTestGeneration/ProgramModification.cs
index fbfc60566d9..5bceb6ea98f 100644
--- a/Source/DafnyTestGeneration/ProgramModification.cs
+++ b/Source/DafnyTestGeneration/ProgramModification.cs
@@ -84,25 +84,6 @@ internal enum Status { Success, Failure, Untested }
     /// Setup DafnyOptions to prepare for counterexample extraction
     /// </summary>
     private static void SetupForCounterexamples(DafnyOptions options) {
-      // Figure out the Z3 version in use:
-      var proverOptions = new SMTLibSolverOptions(options);
-      proverOptions.Parse(options.ProverOptions);
-      var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath);
-      // Based on Z3 version, determine the options to use:
-      var optionsToAdd = new List<string>() {
-        "O:model_evaluator.completion=true",
-        "O:model.completion=true"
-      };
-      if (z3Version is null || z3Version < new Version(4, 8, 6)) {
-        optionsToAdd.Add("O:model_compress=false");
-      } else {
-        optionsToAdd.Add("O:model.compact=false");
-      }
-      // (Re)set the options necessary for counterexample extraction:
-      foreach (var option in optionsToAdd) {
-        options.ProverOptions.RemoveAll(o => o.Split("=") == option.Split("="));
-        options.ProverOptions.Add(option);
-      }
       options.NormalizeNames = false;
       options.EmitDebugInformation = true;
       options.ErrorTrace = 1;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy
index c19005ba48e..215e360a9d1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy
@@ -1,5 +1,5 @@
 
-// RUN: %exits-with 4 %dafny /compile:0 /proverOpt:O:model.compact=false /proverOpt:O:model.completion=true /warnShadowing /extractCounterexample /mv:%t.model "%s" > "%t"
+// RUN: %exits-with 4 %dafny /compile:0 /warnShadowing /extractCounterexample "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The following method performs string equality comparison whereas its 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
index 1aa5726ac5e..27da3845e45 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
@@ -3,23 +3,6 @@ counterexample_commandline.dfy(18,22): Related location: this is the postconditi
 
 Dafny program verifier finished with 1 verified, 1 error
 Counterexample for first failing assertion: 
-counterexample_commandline.dfy(21,8): initial state:
+	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
-	this : Patterns.Simple = (p := @2)
-	@2 : seq<char> = ['?']
-counterexample_commandline.dfy(22,22):
-	s : seq<char> = ['A']
-	this : Patterns.Simple = (p := @2)
-	i : int = 0
-	@2 : seq<char> = ['?']
-counterexample_commandline.dfy(23,12): after some loop iterations:
-	s : seq<char> = ['A']
-	this : Patterns.Simple = (p := @2)
-	i : int = 0
-	@2 : seq<char> = ['?']
-counterexample_commandline.dfy(30,32):
-	s : seq<char> = ['A']
-	this : Patterns.Simple = (p := @2)
-	i : int = 0
-	b : bool = false
-	@2 : seq<char> = ['?']
+	@0 : seq<char> = ['?']

From d5505f444816bfa467e2c0ac63c401642c0871fb Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 16 Nov 2023 04:53:46 -0800
Subject: [PATCH 02/13] Update DafnyRef and dev/news

---
 docs/DafnyRef/Options.txt | 5 +----
 docs/dev/news/4792.fix    | 1 +
 2 files changed, 2 insertions(+), 4 deletions(-)
 create mode 100644 docs/dev/news/4792.fix

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 419f1331c85..77c796b9bb6 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -338,10 +338,7 @@ Usage: dafny [ option ... ] [ filename ... ]
   
   /extractCounterexample
       If verification fails, report a detailed counterexample for the
-      first failing assertion. Requires specifying the /mv:<file> option as well
-      as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
-      /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
-      /proverOpt:O:model.completion=true.
+      first failing assertion (experimental).
   
   ---- Compilation options ---------------------------------------------------
   
diff --git a/docs/dev/news/4792.fix b/docs/dev/news/4792.fix
new file mode 100644
index 00000000000..4a14a30f490
--- /dev/null
+++ b/docs/dev/news/4792.fix
@@ -0,0 +1 @@
+The command line and the language server now use the same counterexample-related Z3 options.

From 8d428bc83d9eb4be3366a6137617ef82b4b0f926 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 16 Nov 2023 05:01:58 -0800
Subject: [PATCH 03/13] Update ProverLogRegression

---
 .../DafnyPipeline.Test/expectedProverLog.smt2 | 20 ++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2
index 5fb530ec4e6..3a03e09c905 100644
--- a/Source/DafnyPipeline.Test/expectedProverLog.smt2
+++ b/Source/DafnyPipeline.Test/expectedProverLog.smt2
@@ -4,10 +4,12 @@
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.arith.solver 2)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 ; done setting options
@@ -218,10 +220,12 @@ $generated@@185)))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.arith.solver 2)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 ; done setting options
@@ -496,10 +500,12 @@ $generated@@226))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.arith.solver 2)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 ; done setting options
@@ -1026,10 +1032,12 @@ $generated@@523))))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.arith.solver 2)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 ; done setting options
@@ -1400,10 +1408,12 @@ $generated@@337)))))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.arith.solver 2)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 ; done setting options

From 77c4e8fb17c7501a174e756821a897d77a9b9096 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 16 Nov 2023 06:03:35 -0800
Subject: [PATCH 04/13] Update existing test

---
 .../LitTest/git-issues/git-issue-2026.dfy     |  2 +-
 .../git-issues/git-issue-2026.dfy.expect      | 25 -------------------
 2 files changed, 1 insertion(+), 26 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
index 4ef2c23f620..3d825c97319 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %dafny /compile:0 "%s" /extractCounterexample /mv model  > "%t"
+// RUN: %exits-with 4 %dafny /compile:0 /extractCounterexample "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // NB: with recent Z3 versions (e.g., 4.12.1), this program no longer
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
index 191893e6a72..d57d862d639 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
@@ -3,30 +3,5 @@ git-issue-2026.dfy(18,18): Related message: loop invariant violation
 
 Dafny program verifier finished with 0 verified, 1 error
 Counterexample for first failing assertion: 
-git-issue-2026.dfy(12,0): initial state:
 	n : int = 2
 	ret : _System.array<seq<char>> = ()
-git-issue-2026.dfy(13,24):
-	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
-	@0 : seq<char> = ['o', 'd', 'd']
-git-issue-2026.dfy(15,14):
-	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
-	i : int = 0
-	@0 : seq<char> = ['o', 'd', 'd']
-git-issue-2026.dfy(16,4): after some loop iterations:
-	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
-	i : int = 0
-	@0 : seq<char> = ['o', 'd', 'd']
-git-issue-2026.dfy(22,27):
-	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
-	i : int = 0
-	@0 : seq<char> = ['o', 'd', 'd']
-git-issue-2026.dfy(26,18):
-	n : int = 2
-	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
-	i : int = 1
-	@0 : seq<char> = ['o', 'd', 'd']

From d182a13f6d336bd9d1378e9c92954447c8d8b94e Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 18 Jan 2024 16:53:42 -0800
Subject: [PATCH 05/13] Enable counterexamples for multiple locations in the
 program

---
 .../Verifier/CaptureStateExtensions.cs          |  4 ++--
 Source/DafnyDriver/CompilerDriver.cs            | 17 ++++++++---------
 .../CounterExampleGeneration/DafnyModelState.cs |  4 ++++
 3 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
index aab81539bb8..0f06ef2b55a 100644
--- a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
+++ b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
@@ -6,7 +6,7 @@ namespace Microsoft.Dafny {
   static class CaptureStateExtensions {
 
     public static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) {
-      if (builder.Options.ModelViewFile != null || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+      if (builder.Options.ExpectingModel) {
         builder.Add(CaptureState(builder.Options, statement));
       }
     }
@@ -18,7 +18,7 @@ static class CaptureStateExtensions {
     }
 
     public static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) {
-      if (builder.Options.ModelViewFile != null || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
+      if (builder.Options.ExpectingModel) {
         builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo));
       }
     }
diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index 84e45308f44..5325e318408 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -354,16 +354,15 @@ public class CompilerDriver : IDisposable {
         return;
       }
       var model = new DafnyModel(firstCounterexample.Model, options);
-      var initialState = model.States.FirstOrDefault(state => state.IsInitialState);
-      if (initialState == null) {
-        return;
-      }
       options.OutputWriter.WriteLine("Counterexample for first failing assertion: ");
-      var vars = initialState.ExpandedVariableSet(-1);
-      foreach (var variable in vars) {
-        options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +
-                                       $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
-                                       $"{variable.Value}");
+      foreach (var state in model.States.Where(state => state.StateContainsPosition())) {
+        options.OutputWriter.WriteLine($"at State {state.FullStateName}:");
+        var vars = state.ExpandedVariableSet(-1);
+        foreach (var variable in vars) {
+          options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +
+                                         $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
+                                         $"{variable.Value}");
+        }
       }
     }
 
diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
index f7632fb2e2c..d2332fa422f 100644
--- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
+++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
@@ -110,6 +110,10 @@ public class DafnyModelState {
 
     public bool IsInitialState => FullStateName.Equals(InitialStateName);
 
+    public bool StateContainsPosition() {
+      return StatePositionRegex.Match(ShortenedStateName).Success;
+    }
+
     public int GetLineId() {
       var match = StatePositionRegex.Match(ShortenedStateName);
       if (!match.Success) {

From 65d2c0478e31fadd9b0b7aae84b3dec3ddfea162 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 18 Jan 2024 16:55:01 -0800
Subject: [PATCH 06/13] Temprorarily add boogie submodule

---
 .gitmodules                       |  4 ++++
 Source/Dafny.sln                  | 38 +++++++++++++++++++++++++++++++
 Source/DafnyCore/DafnyCore.csproj |  2 +-
 boogie                            |  1 +
 4 files changed, 44 insertions(+), 1 deletion(-)
 create mode 160000 boogie

diff --git a/.gitmodules b/.gitmodules
index aa94f844181..c4e3162ea81 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,7 @@
 [submodule "Test/libraries"]
 	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git
+[submodule "bogie"]
+	path = boogie
+	url = https://github.com/Dargones/boogie.git
+	branch = CounterexampleModelFix
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 23297b185ed..fc8e8b1fa49 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -138,5 +164,17 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
+		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index bb4d8aeb517..b6dcd0bbf14 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -32,7 +32,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.9" />
+      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
diff --git a/boogie b/boogie
new file mode 160000
index 00000000000..ac3fc66f6a0
--- /dev/null
+++ b/boogie
@@ -0,0 +1 @@
+Subproject commit ac3fc66f6a0ae5689b017469f2b0cbbcd39aae4a

From 00fa2a5624cab45dd9668133285fb4d9c40afa85 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 18 Jan 2024 17:10:13 -0800
Subject: [PATCH 07/13] Fix test-generation translation pass and Update tests

---
 .../Verifier/CaptureStateExtensions.cs        |  4 +--
 .../git-issues/git-issue-2026.dfy.expect      | 25 +++++++++++++++++++
 .../counterexample_commandline.dfy.expect     | 17 +++++++++++++
 3 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
index 0f06ef2b55a..b406b4aa7a0 100644
--- a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
+++ b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs
@@ -6,7 +6,7 @@ namespace Microsoft.Dafny {
   static class CaptureStateExtensions {
 
     public static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) {
-      if (builder.Options.ExpectingModel) {
+      if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, statement));
       }
     }
@@ -18,7 +18,7 @@ static class CaptureStateExtensions {
     }
 
     public static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) {
-      if (builder.Options.ExpectingModel) {
+      if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo));
       }
     }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
index d57d862d639..e153b0ea870 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
@@ -3,5 +3,30 @@ git-issue-2026.dfy(18,18): Related message: loop invariant violation
 
 Dafny program verifier finished with 0 verified, 1 error
 Counterexample for first failing assertion: 
+at State git-issue-2026.dfy(12,0): initial state:
 	n : int = 2
 	ret : _System.array<seq<char>> = ()
+at State git-issue-2026.dfy(13,24):
+	n : int = 2
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+	@0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(15,14):
+	n : int = 2
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+	i : int = 0
+	@0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(16,4): after some loop iterations:
+	n : int = 2
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
+	i : int = 0
+	@0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(22,27):
+	n : int = 2
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+	i : int = 0
+	@0 : seq<char> = ['o', 'd', 'd']
+at State git-issue-2026.dfy(26,18):
+	n : int = 2
+	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
+	i : int = 1
+	@0 : seq<char> = ['o', 'd', 'd']
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
index 27da3845e45..f56f9407084 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
@@ -3,6 +3,23 @@ counterexample_commandline.dfy(18,22): Related location: this is the postconditi
 
 Dafny program verifier finished with 1 verified, 1 error
 Counterexample for first failing assertion: 
+at State counterexample_commandline.dfy(21,8): initial state:
 	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
 	@0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(22,22):
+	this : Patterns.Simple = (p := @0)
+	s : seq<char> = ['A']
+	i : int = 0
+	@0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(23,12): after some loop iterations:
+	this : Patterns.Simple = (p := @0)
+	s : seq<char> = ['A']
+	i : int = 0
+	@0 : seq<char> = ['?']
+at State counterexample_commandline.dfy(30,32):
+	this : Patterns.Simple = (p := @0)
+	s : seq<char> = ['A']
+	i : int = 0
+	b : bool = false
+	@0 : seq<char> = ['?']

From 0d7789f4633a4a00ee0063490fce4357c7a097db Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Thu, 18 Jan 2024 17:19:27 -0800
Subject: [PATCH 08/13] Fix variable printing order and update tests

---
 Source/DafnyDriver/CompilerDriver.cs                 |  2 +-
 .../CounterExampleGeneration/DafnyModelState.cs      |  4 ++--
 .../Handlers/Custom/DafnyCounterExampleHandler.cs    |  2 +-
 .../LitTest/git-issues/git-issue-2026.dfy.expect     | 12 ++++++------
 .../server/counterexample_commandline.dfy.expect     |  8 ++++----
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs
index 5325e318408..c4d7d72698a 100644
--- a/Source/DafnyDriver/CompilerDriver.cs
+++ b/Source/DafnyDriver/CompilerDriver.cs
@@ -356,7 +356,7 @@ public class CompilerDriver : IDisposable {
       var model = new DafnyModel(firstCounterexample.Model, options);
       options.OutputWriter.WriteLine("Counterexample for first failing assertion: ");
       foreach (var state in model.States.Where(state => state.StateContainsPosition())) {
-        options.OutputWriter.WriteLine($"at State {state.FullStateName}:");
+        options.OutputWriter.WriteLine(state.FullStateName + ":");
         var vars = state.ExpandedVariableSet(-1);
         foreach (var variable in vars) {
           options.OutputWriter.WriteLine($"\t{variable.ShortName} : " +
diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
index d2332fa422f..a04aa9a537d 100644
--- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
+++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs
@@ -56,8 +56,8 @@ public class DafnyModelState {
     /// <param name="maxDepth">The maximum depth up to which to expand the
     /// variable set.</param>
     /// <returns>Set of variables</returns>
-    public HashSet<DafnyModelVariable> ExpandedVariableSet(int maxDepth) {
-      HashSet<DafnyModelVariable> expandedSet = new();
+    public List<DafnyModelVariable> ExpandedVariableSet(int maxDepth) {
+      List<DafnyModelVariable> expandedSet = new();
       // The following is the queue for elements to be added to the set. The 2nd
       // element of a tuple is the depth of the variable w.r.t. the original set
       List<Tuple<DafnyModelVariable, int>> varsToAdd = new();
diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
index 98dace07a08..7e35a842a2e 100644
--- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
@@ -106,7 +106,7 @@ private class CounterExampleLoader {
       }
 
       private CounterExampleItem GetCounterExample(DafnyModelState state) {
-        HashSet<DafnyModelVariable> vars = state.ExpandedVariableSet(counterExampleDepth);
+        List<DafnyModelVariable> vars = state.ExpandedVariableSet(counterExampleDepth);
         return new(
           new Position(state.GetLineId() - 1, state.GetCharId()),
           vars.WithCancellation(cancellationToken).ToDictionary(
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
index e153b0ea870..191893e6a72 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy.expect
@@ -3,29 +3,29 @@ git-issue-2026.dfy(18,18): Related message: loop invariant violation
 
 Dafny program verifier finished with 0 verified, 1 error
 Counterexample for first failing assertion: 
-at State git-issue-2026.dfy(12,0): initial state:
+git-issue-2026.dfy(12,0): initial state:
 	n : int = 2
 	ret : _System.array<seq<char>> = ()
-at State git-issue-2026.dfy(13,24):
+git-issue-2026.dfy(13,24):
 	n : int = 2
 	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	@0 : seq<char> = ['o', 'd', 'd']
-at State git-issue-2026.dfy(15,14):
+git-issue-2026.dfy(15,14):
 	n : int = 2
 	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
-at State git-issue-2026.dfy(16,4): after some loop iterations:
+git-issue-2026.dfy(16,4): after some loop iterations:
 	n : int = 2
 	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
-at State git-issue-2026.dfy(22,27):
+git-issue-2026.dfy(22,27):
 	n : int = 2
 	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 0
 	@0 : seq<char> = ['o', 'd', 'd']
-at State git-issue-2026.dfy(26,18):
+git-issue-2026.dfy(26,18):
 	n : int = 2
 	ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
 	i : int = 1
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
index f56f9407084..c889c99e509 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect
@@ -3,21 +3,21 @@ counterexample_commandline.dfy(18,22): Related location: this is the postconditi
 
 Dafny program verifier finished with 1 verified, 1 error
 Counterexample for first failing assertion: 
-at State counterexample_commandline.dfy(21,8): initial state:
+counterexample_commandline.dfy(21,8): initial state:
 	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
 	@0 : seq<char> = ['?']
-at State counterexample_commandline.dfy(22,22):
+counterexample_commandline.dfy(22,22):
 	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
 	i : int = 0
 	@0 : seq<char> = ['?']
-at State counterexample_commandline.dfy(23,12): after some loop iterations:
+counterexample_commandline.dfy(23,12): after some loop iterations:
 	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
 	i : int = 0
 	@0 : seq<char> = ['?']
-at State counterexample_commandline.dfy(30,32):
+counterexample_commandline.dfy(30,32):
 	this : Patterns.Simple = (p := @0)
 	s : seq<char> = ['A']
 	i : int = 0

From 8aa183b86387de4e8375bf86a85d63685442d02a Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Mon, 22 Jan 2024 09:10:45 -0800
Subject: [PATCH 09/13] Revert "Temprorarily add boogie submodule"

This reverts commit 65d2c0478e31fadd9b0b7aae84b3dec3ddfea162.
---
 .gitmodules                       |  4 ----
 Source/Dafny.sln                  | 38 -------------------------------
 Source/DafnyCore/DafnyCore.csproj |  2 +-
 boogie                            |  1 -
 4 files changed, 1 insertion(+), 44 deletions(-)
 delete mode 160000 boogie

diff --git a/.gitmodules b/.gitmodules
index c4e3162ea81..aa94f844181 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,7 +1,3 @@
 [submodule "Test/libraries"]
 	path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries
 	url = https://github.com/dafny-lang/libraries.git
-[submodule "bogie"]
-	path = boogie
-	url = https://github.com/Dargones/boogie.git
-	branch = CounterexampleModelFix
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index fc8e8b1fa49..23297b185ed 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -43,32 +43,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
-Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
-EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -164,17 +138,5 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
-		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
-		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index b6dcd0bbf14..bb4d8aeb517 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -32,7 +32,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
-      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.9" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
diff --git a/boogie b/boogie
deleted file mode 160000
index ac3fc66f6a0..00000000000
--- a/boogie
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit ac3fc66f6a0ae5689b017469f2b0cbbcd39aae4a

From 10002e4dc53936245aa2543737fda19b770914e8 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Mon, 22 Jan 2024 09:17:37 -0800
Subject: [PATCH 10/13] Update Boogie version

---
 Source/DafnyCore/DafnyCore.csproj | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index bb4d8aeb517..13cfdb24455 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -32,7 +32,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.9" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.10" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

From 76700d763f4f182672f336297963efc8dc63e5ce Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Mon, 22 Jan 2024 09:20:01 -0800
Subject: [PATCH 11/13] Fix customBoogie.patchj

---
 customBoogie.patch | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/customBoogie.patch b/customBoogie.patch
index 3648e35e5dd..becfb63f2f8 100644
--- a/customBoogie.patch
+++ b/customBoogie.patch
@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
        <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
        <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
        <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
--      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.9" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.10" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

From 8515c8e7ad35b1679b7b1bc06a05f00ad6641ee5 Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Mon, 22 Jan 2024 11:11:46 -0800
Subject: [PATCH 12/13] Update Prover Log test

---
 .../DafnyPipeline.Test/expectedProverLog.smt2 | 20 ++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2
index 6f25c728cd7..da96d1c80f2 100644
--- a/Source/DafnyPipeline.Test/expectedProverLog.smt2
+++ b/Source/DafnyPipeline.Test/expectedProverLog.smt2
@@ -200,9 +200,11 @@
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 (set-option :smt.arith.solver 2)
@@ -490,9 +492,11 @@ $generated@@185)))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 (set-option :smt.arith.solver 2)
@@ -1030,9 +1034,11 @@ $generated@@226))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 (set-option :smt.arith.solver 2)
@@ -1413,9 +1419,11 @@ $generated@@523))))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 (set-option :smt.arith.solver 2)
@@ -1938,9 +1946,11 @@ $generated@@337)))))))))
 (set-option :type_check true)
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.delay_units true)
+(set-option :model_evaluator.completion true)
+(set-option :model.completion true)
+(set-option :model.compact false)
 (set-option :smt.case_split 3)
 (set-option :smt.mbqi false)
-(set-option :model.compact false)
 (set-option :model.v2 true)
 (set-option :pp.bv_literals false)
 (set-option :smt.arith.solver 2)

From c06d769b877c732b4294a781df1b9651cb81eb3d Mon Sep 17 00:00:00 2001
From: Aleksandr Fedchin <fedchina@amazon.com>
Date: Mon, 22 Jan 2024 12:25:11 -0800
Subject: [PATCH 13/13] Update Inverses test

---
 .../TestFiles/LitTests/LitTest/dafny0/Inverses.dfy.expect       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Inverses.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Inverses.dfy.expect
index 0721e08565c..ad7225bfbe9 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Inverses.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Inverses.dfy.expect
@@ -2,7 +2,7 @@ Inverses.dfy(68,0): Error: a postcondition could not be proved on this return pa
 Inverses.dfy(67,10): Related location: this is the postcondition that could not be proved
 Inverses.dfy(80,0): Error: a postcondition could not be proved on this return path
 Inverses.dfy(79,10): Related location: this is the postcondition that could not be proved
-Inverses.dfy(193,2): Error: a postcondition could not be proved on this return path
+Inverses.dfy(192,0): Error: a postcondition could not be proved on this return path
 Inverses.dfy(191,15): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 31 verified, 3 errors