From 5975ea77f4ee9ef80a5ca2b2245db782a36019dc Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Thu, 21 Mar 2024 08:41:52 -0700 Subject: [PATCH] Add a warning indicating that the counterexample may be inconsistent of invalid --- .../DafnyDriver/Legacy/SynchronousCliCompilation.cs | 1 + docs/DafnyRef/UserGuide.md | 12 ++++++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index d567cac9a6d..204d76a4831 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -352,6 +352,7 @@ private static void PrintCounterexample(DafnyOptions options) { } var model = new DafnyModel(firstCounterexample.Model, options); model.AssignConcretePrimitiveValues(); + options.OutputWriter.WriteLine("WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#fn:smt-encoding."); options.OutputWriter.WriteLine("Counterexample for first failing assertion: "); if (model.LoopGuards.Count > 0) { options.OutputWriter.WriteLine("Temporary variables to describe counterexamples: "); diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 0c4ec18adc1..56b504b9d09 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -2469,12 +2469,12 @@ Legacy options: * `1` (default) - in the body of prefix lemmas, rewrite any use of a focal predicate `P` to `P#[_k-1]`. -* `-extractCounterexample` - control generation of counterexamples. If - verification fails, report a detailed counterexample for the first - failing assertion. Requires specifying the `-mv` option, to specify - where to write the counterexample, as well as the - `-proverOpt:O:model_compress=false` and - `-proverOpt:O:model.completion=true` options. +* `-extractCounterexample` - if verification fails, report a possible + counterexample as a set of assumptions that can be inserted into the code. + Note that Danfy cannot guarantee that the counterexample + it reports provably violates the assertion or that the assumptions are not + mutually inconsistent (see [^smt-encoding]), so this output should be + expected manually and treated as a hint. ### 13.9.8. Controlling compilation {#sec-controlling-compilation}