diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 4182ff58051..052b4fef298 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 VCResults); + List VCResults, + List 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/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 @@ - + diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index e482fd02c74..58e8e31cef7 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/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: 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 11de3dee370..34d7fb0bb25 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/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 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 option, Boogie.CommandLineParseState ps, } }); + DafnyOptions.RegisterLegacyBinding(ExtractCounterexample, (options, value) => { + options.ExtractCounterexample = value; + options.EnhancedErrorMessages = 1; + }); + DooFile.RegisterLibraryChecks( new Dictionary() { { UnicodeCharacters, DooFile.CheckOptionMatches }, @@ -553,8 +563,9 @@ void ParsePrintMode(Option option, Boogie.CommandLineParseState ps, OptimizeErasableDatatypeWrapper, AddCompileSuffix, SystemModule, - ExecutionCoverageReport - ); + ExecutionCoverageReport, + ExtractCounterexample + ); } public static readonly Option FormatPrint = new("--print", diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 68b208299ae..e0596901553 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -45,6 +45,7 @@ static DafnyCommands() { CommonOptionBag.WarnRedundantAssumptions, CommonOptionBag.NoTimeStampForCoverageReport, CommonOptionBag.VerificationCoverageReport, + CommonOptionBag.ExtractCounterexample, CommonOptionBag.ShowInference, CommonOptionBag.ManualTriggerOption }.ToList(); diff --git a/Source/DafnyCore/Verifier/CaptureStateExtensions.cs b/Source/DafnyCore/Verifier/CaptureStateExtensions.cs index aab81539bb8..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.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)); } } diff --git a/Source/DafnyDriver/CompilerDriver.cs b/Source/DafnyDriver/CompilerDriver.cs index b913ed9534c..c4d7d72698a 100644 --- a/Source/DafnyDriver/CompilerDriver.cs +++ b/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 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 ProcessFilesAsync(IReadOnlyList/*!* 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 ProcessFilesAsync(IReadOnlyList/*!* /// Extract the counterexample corresponding to the first failing /// assertion and print it to the console /// - 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}"); } } } diff --git a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs index f7632fb2e2c..a04aa9a537d 100644 --- a/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs +++ b/Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModelState.cs @@ -56,8 +56,8 @@ internal DafnyModelState(DafnyModel model, Model.CapturedState state) { /// The maximum depth up to which to expand the /// variable set. /// Set of variables - public HashSet ExpandedVariableSet(int maxDepth) { - HashSet expandedSet = new(); + public List ExpandedVariableSet(int maxDepth) { + List 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> 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) { 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 IEnumerable GetCounterExamples(DafnyModel model) { } private CounterExampleItem GetCounterExample(DafnyModelState state) { - HashSet vars = state.ExpandedVariableSet(counterExampleDepth); + List vars = state.ExpandedVariableSet(counterExampleDepth); return new( new Position(state.GetLineId() - 1, state.GetCharId()), vars.WithCancellation(cancellationToken).ToDictionary( diff --git a/Source/DafnyLanguageServer/LanguageServer.cs b/Source/DafnyLanguageServer/LanguageServer.cs index ba700ecf2b5..f7ad5c1a07c 100644 --- a/Source/DafnyLanguageServer/LanguageServer.cs +++ b/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() - { - "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/DafnyPipeline.Test/expectedProverLog.smt2 b/Source/DafnyPipeline.Test/expectedProverLog.smt2 index ba23b9ae4d4..da96d1c80f2 100644 --- a/Source/DafnyPipeline.Test/expectedProverLog.smt2 +++ b/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) 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 @@ public ProgramModification(DafnyOptions options, Program program, Implementation /// Setup DafnyOptions to prepare for counterexample extraction /// 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() { - "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/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 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/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..c889c99e509 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/counterexample_commandline.dfy.expect @@ -4,22 +4,22 @@ 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 = ['A'] - this : Patterns.Simple = (p := @2) - @2 : seq = ['?'] + @0 : seq = ['?'] counterexample_commandline.dfy(22,22): + this : Patterns.Simple = (p := @0) s : seq = ['A'] - this : Patterns.Simple = (p := @2) i : int = 0 - @2 : seq = ['?'] + @0 : seq = ['?'] counterexample_commandline.dfy(23,12): after some loop iterations: + this : Patterns.Simple = (p := @0) s : seq = ['A'] - this : Patterns.Simple = (p := @2) i : int = 0 - @2 : seq = ['?'] + @0 : seq = ['?'] counterexample_commandline.dfy(30,32): + this : Patterns.Simple = (p := @0) s : seq = ['A'] - this : Patterns.Simple = (p := @2) i : int = 0 b : bool = false - @2 : seq = ['?'] + @0 : seq = ['?'] 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 -- +- + + + diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 405096d5851..945e8c2e645 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -342,10 +342,7 @@ Usage: dafny [ option ... ] [ filename ... ] /extractCounterexample If verification fails, report a detailed counterexample for the - first failing assertion. Requires specifying the /mv: 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.