Counterexamples As Assumptions

Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs

@@ -1510,7 +1510,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr,
       }
 
       var loopBodyBuilder = new BoogieStmtListBuilder(this, options);
-      loopBodyBuilder.AddCaptureState(s.Tok, true, "after some loop iterations");
+      loopBodyBuilder.AddCaptureState(s.Tok, true, CaptureStateExtensions.AfterLoopIterationsStateMarker);
 
       // As the first thing inside the loop, generate:  if (!w) { CheckWellformed(inv); assume false; }
       invDefinednessBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False));

Source/DafnyCore/Verifier/CaptureStateExtensions.cs

@@ -3,9 +3,11 @@
 using Bpl = Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
-  static class CaptureStateExtensions {
+  public static class CaptureStateExtensions {
 
-    public static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) {
+    public const string AfterLoopIterationsStateMarker = "after some loop iterations";
+
+    internal static void AddCaptureState(this BoogieStmtListBuilder builder, Statement statement) {
       if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, statement));
       }
@@ -17,7 +19,7 @@ private static Bpl.Cmd CaptureState(DafnyOptions options, Statement stmt) {
       return CaptureState(options, stmt.RangeToken.EndToken, true, null);
     }
 
-    public static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) {
+    internal static void AddCaptureState(this BoogieStmtListBuilder builder, IToken tok, bool isEndToken, string /*?*/ additionalInfo) {
       if (builder.Options.ExpectingModel || builder.Options.TestGenOptions.Mode != TestGenerationOptions.Modes.None) {
         builder.Add(CaptureState(builder.Options, tok, isEndToken, additionalInfo));
       }

Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs

@@ -351,15 +351,18 @@ private static void PrintCounterexample(DafnyOptions options) {
         return;
       }
       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: ");
+        foreach (var loopGuard in model.LoopGuards) {
+          options.OutputWriter.WriteLine($"ghost var {loopGuard} : bool := false;");
+        }
+      }
       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}");
-        }
+        options.OutputWriter.WriteLine(state.AsAssumption());
       }
     }