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 @@ public enum IncludesModes {
 
  case "extractCounterexample":
  ExtractCounterexample = true;
+ EnhancedErrorMessages = 1;
  return true;
 
  case "verificationLogger":
@@ -1146,6 +1147,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
@@ -1412,10 +1420,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 ---------------------------------------------------
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -308,6 +308,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.RegisterLegacyBinding(ShowInference, (options, value) => {
  options.PrintTooltips = value;
@@ -503,6 +508,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 },
@@ -553,8 +563,9 @@ public enum DefaultFunctionOpacityOptions {
  OptimizeErasableDatatypeWrapper,
  AddCompileSuffix,
  SystemModule,
- ExecutionCoverageReport
- );
+ ExecutionCoverageReport,
+ ExtractCounterexample
+ );
  }
 
  public static readonly Option<bool> FormatPrint = new("--print",

Source/DafnyCore/Options/DafnyCommands.cs

@@ -45,6 +45,7 @@ public static class 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 @@ 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.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 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);
@@ -338,7 +333,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;
  }
@@ -347,16 +342,26 @@ 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);
  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 @@ 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();
@@ -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) {

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(

Source/DafnyLanguageServer/LanguageServer.cs

@@ -53,13 +53,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) {

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

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