Parity in Counterexample-Related Z3 Options for Command-Line vs Language Server

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) {

Source/DafnyCore/DafnyOptions.cs

@@ -729,6 +729,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
 
         case "extractCounterexample":
           ExtractCounterexample = true;
+          EnhancedErrorMessages = 1;
           return true;
 
         case "verificationLogger":
@@ -1148,6 +1149,13 @@ public void SetZ3Options(Version z3Version) {
       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 @@ focal predicate P to P#[_k-1].
 
 /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 ---------------------------------------------------
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -291,6 +291,11 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis
 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 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
         }
       });
 
+    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 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       OptimizeErasableDatatypeWrapper,
       AddCompileSuffix,
       SystemModule,
-      ExecutionCoverageReport
-    );
+      ExecutionCoverageReport,
+      ExtractCounterexample
+      );
   }
 
   public static readonly Option<bool> FormatPrint = new("--print",

Source/DafnyCore/Options/DafnyCommands.cs

@@ -43,7 +43,8 @@ static DafnyCommands() {
     CommonOptionBag.WarnContradictoryAssumptions,
     CommonOptionBag.WarnRedundantAssumptions,
     CommonOptionBag.NoTimeStampForCoverageReport,
-    CommonOptionBag.VerificationCoverageReport
+    CommonOptionBag.VerificationCoverageReport,
+    CommonOptionBag.ExtractCounterexample
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {

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 static async Task<int> RunCompiler(DafnyOptions options) {
         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 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
         Util.PrintFunctionCallGraph(dafnyProgram);
       }
       if (dafnyProgram != null && options.ExtractCounterexample && exitValue == ExitValue.VERIFICATION_ERROR) {
-        PrintCounterexample(options, options.ModelViewFile);
+        PrintCounterexample(options);
       }
       return exitValue;
     }
@@ -196,17 +191,28 @@ private async Task<ExitValue> ProcessFilesAsync(IReadOnlyList<DafnyFile/*!*/>/*!
     /// 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}");
       }
     }
 

Source/DafnyLanguageServer/LanguageServer.cs

@@ -54,13 +54,6 @@ public static void ConfigureDafnyOptionsForServer(DafnyOptions dafnyOptions) {
       //      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) {

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

Source/DafnyTestGeneration/ProgramModification.cs

@@ -84,25 +84,6 @@ public ProgramModification(DafnyOptions options, Program program, Implementation
     /// 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;

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

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']

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 

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> = ['?']

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 ---------------------------------------------------
 

docs/dev/news/4792.fix

@@ -0,0 +1 @@
+The command line and the language server now use the same counterexample-related Z3 options.