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

Source/DafnyCore/DafnyOptions.cs

@@ -723,6 +723,7 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
 
         case "extractCounterexample":
           ExtractCounterexample = true;
+          EnhancedErrorMessages = 1;
           return true;
 
         case "verificationLogger":
@@ -1146,6 +1147,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
@@ -1412,10 +1420,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

@@ -308,6 +308,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.RegisterLegacyBinding(ShowInference, (options, value) => {
       options.PrintTooltips = value;
@@ -503,6 +508,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 },
@@ -553,8 +563,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

@@ -45,6 +45,7 @@ static DafnyCommands() {
     CommonOptionBag.WarnRedundantAssumptions,
     CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport,
+    CommonOptionBag.ExtractCounterexample,
     CommonOptionBag.ShowInference,
     CommonOptionBag.ManualTriggerOption
   }.ToList();

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.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, statement));
       }
     }
@@ -18,7 +18,7 @@ private static Bpl.Cmd CaptureState(DafnyOptions options, Statement stmt) {
     }
 
     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.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo));
       }
     }

Source/DafnyDriver/CompilerDriver.cs

@@ -26,6 +26,7 @@
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer.CounterExampleGeneration;
 using Microsoft.Dafny.Plugins;
+using VC;
 
 namespace Microsoft.Dafny {
 
@@ -56,12 +57,6 @@ public static async Task<int> Run(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);
@@ -338,7 +333,7 @@ public 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;
     }
@@ -347,16 +342,26 @@ public 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);
       options.OutputWriter.WriteLine("Counterexample for first failing assertion: ");
-      foreach (var state in model.States.Where(state => !state.IsInitialState)) {
+      foreach (var state in model.States.Where(state => state.StateContainsPosition())) {
         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}");
+                                         $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
+                                         $"{variable.Value}");
         }
       }
     }

Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs

@@ -56,8 +56,8 @@ internal DafnyModelState(DafnyModel model, Model.CapturedState state) {
     /// <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();
@@ -110,6 +110,10 @@ internal bool VarNameIsShared(string name) {
 
     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) {

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs

@@ -106,7 +106,7 @@ private IEnumerable<CounterExampleItem> GetCounterExamples(DafnyModel model) {
       }
 
       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(

Source/DafnyLanguageServer/LanguageServer.cs

@@ -53,13 +53,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,9 +4,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)
@@ -198,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)
@@ -229,9 +233,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)
@@ -486,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)
@@ -518,9 +526,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)
@@ -1024,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)
@@ -1058,9 +1070,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)
@@ -1405,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)
@@ -1442,9 +1458,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)
@@ -1928,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)

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

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