From 2e6a08c2882d10caa5f6bbfef09c5b1bdd31752f Mon Sep 17 00:00:00 2001
From: Alex Chew <alex-chew@users.noreply.github.com>
Date: Fri, 19 Apr 2024 17:29:20 -0700
Subject: [PATCH] Add first pass of proof obligation description expressions
 (#5317)

### Description
Adds a first pass of proof obligation description expressions, towards
resolving https://github.com/dafny-lang/dafny/issues/2987. It also adds
a new hidden option, `--show-proof-obligation-expressions`, which adds
to each (supported) failed proof obligation error message an equivalent
Dafny assertion. This option is used to automate tests for the newly
added proof obligation description expressions, but this PR does not
backfill tests for existing PODesc expressions.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
---
 Source/DafnyCore/DafnyOptions.cs              |   6 +
 .../DafnyCore/Generic/ReporterExtensions.cs   |   3 +-
 Source/DafnyCore/Options/CommonOptionBag.cs   |  13 +-
 Source/DafnyCore/Options/DafnyCommands.cs     |   3 +-
 Source/DafnyCore/Pipeline/Compilation.cs      |  38 +++
 .../BoogieGenerator.ExpressionWellformed.cs   |  56 ++--
 .../Verifier/BoogieGenerator.Functions.cs     |   2 +-
 .../Verifier/BoogieGenerator.Methods.cs       |   7 +-
 .../Verifier/BoogieGenerator.TrStatement.cs   |  41 ++-
 .../Verifier/BoogieGenerator.Types.cs         |  68 +++--
 Source/DafnyCore/Verifier/BoogieGenerator.cs  |   2 +-
 .../Verifier/ProofObligationDescription.cs    | 271 ++++++++++++++++--
 .../array-init-empty.dfy                      |   6 +
 .../array-init-empty.dfy.expect               |   4 +
 .../array-init-size-valid.dfy                 |   6 +
 .../array-init-size-valid.dfy.expect          |   4 +
 .../char-overflow-non-unicode.dfy             |   6 +
 .../char-overflow-non-unicode.dfy.expect      |   5 +
 .../char-overflow-unicode.dfy                 |   6 +
 .../char-overflow-unicode.dfy.expect          |   4 +
 .../char-underflow-non-unicode.dfy            |   6 +
 .../char-underflow-non-unicode.dfy.expect     |   5 +
 .../char-underflow-unicode.dfy                |   6 +
 .../char-underflow-unicode.dfy.expect         |   4 +
 .../proof-obligation-desc/conversion-fit.dfy  |   7 +
 .../conversion-fit.dfy.expect                 |   4 +
 .../conversion-is-natural.dfy                 |   7 +
 .../conversion-is-natural.dfy.expect          |   4 +
 .../conversion-positive.dfy                   |   7 +
 .../conversion-positive.dfy.expect            |   4 +
 .../conversion-satisfies-constraints.dfy      |   9 +
 ...onversion-satisfies-constraints.dfy.expect |   4 +
 .../for-range-assignable.dfy                  |   7 +
 .../for-range-assignable.dfy.expect           |   4 +
 .../for-range-bounds-valid.dfy                |   7 +
 .../for-range-bounds-valid.dfy.expect         |   4 +
 .../forall-postcondition.dfy                  |   7 +
 .../forall-postcondition.dfy.expect           |   5 +
 .../proof-obligation-desc/is-allocated.dfy    |  12 +
 .../is-allocated.dfy.expect                   |   4 +
 .../proof-obligation-desc/is-integer.dfy      |   7 +
 .../is-integer.dfy.expect                     |   4 +
 .../proof-obligation-desc/non-negative.dfy    |   7 +
 .../non-negative.dfy.expect                   |   4 +
 .../proof-obligation-desc/non-null.dfy        |   7 +
 .../proof-obligation-desc/non-null.dfy.expect |   4 +
 .../ordinal-subtraction-is-natural.dfy        |   8 +
 .../ordinal-subtraction-is-natural.dfy.expect |   4 +
 .../ordinal-subtraction-underflow.dfy         |   8 +
 .../ordinal-subtraction-underflow.dfy.expect  |   4 +
 .../shift-lower-bound.dfy                     |   6 +
 .../shift-lower-bound.dfy.expect              |   4 +
 .../shift-upper-bound.dfy                     |   6 +
 .../shift-upper-bound.dfy.expect              |   4 +
 .../proof-obligation-desc/witness-check.dfy   |   4 +
 .../witness-check.dfy.expect                  |   4 +
 56 files changed, 666 insertions(+), 87 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index ad51aac125..f5855a8962 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -380,6 +380,8 @@ public enum IncludesModes {
     [CanBeNull] private TestGenerationOptions testGenOptions = null;
     public bool ExtractCounterexample = false;
 
+    public bool ShowProofObligationExpressions = false;
+
     public bool AuditProgram = false;
 
     public static string DefaultZ3Version = "4.12.1";
@@ -796,6 +798,10 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
           EnhancedErrorMessages = 1;
           return true;
 
+        case "showProofObligationExpressions":
+          ShowProofObligationExpressions = true;
+          return true;
+
         case "testContracts":
           if (ps.ConfirmArgumentCount(1)) {
             if (args[ps.i].Equals("Externs")) {
diff --git a/Source/DafnyCore/Generic/ReporterExtensions.cs b/Source/DafnyCore/Generic/ReporterExtensions.cs
index 2c7db25491..579cea5939 100644
--- a/Source/DafnyCore/Generic/ReporterExtensions.cs
+++ b/Source/DafnyCore/Generic/ReporterExtensions.cs
@@ -11,7 +11,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
     var usingSnippets = reporter.Options.Get(Snippets.ShowSnippets);
     var relatedInformation = new List<DafnyRelatedInformation>();
     foreach (var auxiliaryInformation in error.Aux) {
-      if (auxiliaryInformation.Category == RelatedMessageCategory) {
+      if (auxiliaryInformation.Category == RelatedMessageCategory || auxiliaryInformation.Category == AssertedExprCategory) {
         error.Msg += "\n" + auxiliaryInformation.FullMsg;
       } else if (auxiliaryInformation.Category == RelatedLocationCategory) {
         relatedInformation.AddRange(CreateDiagnosticRelatedInformationFor(BoogieGenerator.ToDafnyToken(true, auxiliaryInformation.Tok), auxiliaryInformation.Msg, usingSnippets));
@@ -46,6 +46,7 @@ public static void ReportBoogieError(this ErrorReporter reporter, ErrorInformati
   private const string RelatedLocationCategory = "Related location";
   public const string RelatedLocationMessage = RelatedLocationCategory;
   private const string RelatedMessageCategory = "Related message";
+  public const string AssertedExprCategory = "Asserted expression";
   public static readonly string PostConditionFailingMessage = new ProofObligationDescription.EnsuresDescription(null, null).FailureDescription;
   private static string FormatRelated(string related) {
     return $"Could not prove: {related}";
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index f461a222ec..ef7563b8a0 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -359,6 +359,12 @@ Allow Dafny code to depend on the standard libraries included with the Dafny dis
 If verification fails, report a detailed counterexample for the first failing assertion (experimental).".TrimStart()) {
   };
 
+  public static readonly Option<bool> ShowProofObligationExpressions = new("--show-proof-obligation-expressions", () => false,
+    @"
+(Experimental) Show Dafny expressions corresponding to unverified proof obligations.".TrimStart()) {
+    IsHidden = true
+  };
+
   static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(WarnAsErrors, (options, value) => {
       if (!options.Get(AllowWarnings) && !options.Get(WarnAsErrors)) {
@@ -571,6 +577,10 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       options.EnhancedErrorMessages = 1;
     });
 
+    DafnyOptions.RegisterLegacyBinding(ShowProofObligationExpressions, (options, value) => {
+      options.ShowProofObligationExpressions = value;
+    });
+
     DooFile.RegisterLibraryChecks(
       new Dictionary<Option, DooFile.OptionCheck>() {
         { UnicodeCharacters, DooFile.CheckOptionMatches },
@@ -635,7 +645,8 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       AddCompileSuffix,
       SystemModule,
       ExecutionCoverageReport,
-      ExtractCounterexample
+      ExtractCounterexample,
+      ShowProofObligationExpressions
       );
   }
 
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index a0e8f66cb5..d482ab458f 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -48,7 +48,8 @@ static DafnyCommands() {
     CommonOptionBag.NoTimeStampForCoverageReport,
     CommonOptionBag.VerificationCoverageReport,
     CommonOptionBag.ExtractCounterexample,
-    CommonOptionBag.ManualTriggerOption
+    CommonOptionBag.ManualTriggerOption,
+    CommonOptionBag.ShowProofObligationExpressions
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {
diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
index 117902d98b..4b37916dec 100644
--- a/Source/DafnyCore/Pipeline/Compilation.cs
+++ b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -14,6 +14,7 @@
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using VC;
+using VCGeneration;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny;
@@ -518,6 +519,9 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
     foreach (var counterExample in result.CounterExamples) //.OrderBy(d => d.GetLocation()))
     {
       var errorInformation = counterExample.CreateErrorInformation(outcome, options.ForceBplErrors);
+      if (options.ShowProofObligationExpressions) {
+        AddAssertedExprToCounterExampleErrorInfo(options, counterExample, errorInformation);
+      }
       var dafnyCounterExampleModel = options.ExtractCounterexample ? new DafnyModel(counterExample.Model, options) : null;
       errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel);
     }
@@ -531,6 +535,40 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
       timeLimit, result.CounterExamples);
   }
 
+  private static void AddAssertedExprToCounterExampleErrorInfo(
+      DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) {
+    Boogie.ProofObligationDescription? boogieProofObligationDesc = null;
+    switch (errorInformation.Kind) {
+      case ErrorKind.Assertion:
+        boogieProofObligationDesc = ((AssertCounterexample)counterExample).FailingAssert.Description;
+        break;
+      case ErrorKind.Precondition:
+        boogieProofObligationDesc = ((CallCounterexample)counterExample).FailingCall.Description;
+        break;
+      case ErrorKind.Postcondition:
+        boogieProofObligationDesc = ((ReturnCounterexample)counterExample).FailingReturn.Description;
+        break;
+      case ErrorKind.InvariantEntry:
+      case ErrorKind.InvariantMaintainance:
+        AssertCmd failingAssert = ((AssertCounterexample)counterExample).FailingAssert;
+        if (failingAssert is LoopInitAssertCmd loopInitAssertCmd) {
+          boogieProofObligationDesc = loopInitAssertCmd.originalAssert.Description;
+        } else if (failingAssert is LoopInvMaintainedAssertCmd maintainedAssertCmd) {
+          boogieProofObligationDesc = maintainedAssertCmd.originalAssert.Description;
+        }
+        break;
+      default:
+        throw new ArgumentOutOfRangeException($"Unexpected ErrorKind: {errorInformation.Kind}");
+    }
+
+    if (boogieProofObligationDesc is ProofObligationDescription.ProofObligationDescription dafnyProofObligationDesc) {
+      var expr = dafnyProofObligationDesc.GetAssertedExpr(options);
+      if (expr != null) {
+        errorInformation.AddAuxInfo(errorInformation.Tok, expr.ToString(), ErrorReporterExtensions.AssertedExprCategory);
+      }
+    }
+  }
+
   public static VcOutcome GetOutcome(SolverOutcome outcome) {
     switch (outcome) {
       case SolverOutcome.Valid:
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
index 784c2ed116..eee27a5cdb 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
@@ -361,14 +361,14 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
               if (e.Member is TwoStateFunction) {
                 Bpl.Expr wh = GetWhereClause(selectExpr.tok, etran.TrExpr(e.Obj), e.Obj.Type, etran.OldAt(e.AtLabel), ISALLOC, true);
                 if (wh != null) {
-                  var desc = new PODesc.IsAllocated("receiver argument", "in the two-state function's previous state");
+                  var desc = new PODesc.IsAllocated("receiver argument", "in the two-state function's previous state", e.Obj, e.AtLabel);
                   builder.Add(Assert(GetToken(expr), wh, desc));
                 }
               } else if (etran.UsesOldHeap) {
                 Bpl.Expr wh = GetWhereClause(selectExpr.tok, etran.TrExpr(e.Obj), e.Obj.Type, etran, ISALLOC, true);
                 if (wh != null) {
                   var desc = new PODesc.IsAllocated("receiver",
-                    $"in the state in which its {(e.Member is Field ? "fields" : "members")} are accessed");
+                    $"in the state in which its {(e.Member is Field ? "fields" : "members")} are accessed", e.Obj, e.AtLabel);
                   builder.Add(Assert(GetToken(expr), wh, desc));
                 }
               }
@@ -387,9 +387,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             CheckWellformed(e.Seq, wfOptions, locals, builder, etran);
             Bpl.Expr seq = etran.TrExpr(e.Seq);
             if (eSeqType.IsArrayType) {
-              builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, predef.Null), new PODesc.NonNull("array")));
+              builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, predef.Null), new PODesc.NonNull("array", e.Seq)));
               if (etran.UsesOldHeap) {
-                builder.Add(Assert(GetToken(e.Seq), MkIsAlloc(seq, eSeqType, etran.HeapExpr), new PODesc.IsAllocated("array", null)));
+                builder.Add(Assert(GetToken(e.Seq), MkIsAlloc(seq, eSeqType, etran.HeapExpr), new PODesc.IsAllocated("array", null, e.Seq)));
               }
             }
             Bpl.Expr e0 = null;
@@ -458,9 +458,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             MultiSelectExpr e = selectExpr;
             CheckWellformed(e.Array, wfOptions, locals, builder, etran);
             Bpl.Expr array = etran.TrExpr(e.Array);
-            builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, predef.Null), new PODesc.NonNull("array")));
+            builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, predef.Null), new PODesc.NonNull("array", e.Array)));
             if (etran.UsesOldHeap) {
-              builder.Add(Assert(GetToken(e.Array), MkIsAlloc(array, e.Array.Type, etran.HeapExpr), new PODesc.IsAllocated("array", null)));
+              builder.Add(Assert(GetToken(e.Array), MkIsAlloc(array, e.Array.Type, etran.HeapExpr), new PODesc.IsAllocated("array", null, e.Array)));
             }
             for (int idxId = 0; idxId < e.Indices.Count; idxId++) {
               var idx = e.Indices[idxId];
@@ -506,7 +506,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             } else if (collectionType is MapType mapType) {
               CheckSubrange(e.Value.tok, value, e.Value.Type, mapType.Range, builder);
             } else if (collectionType is MultiSetType) {
-              var desc = new PODesc.NonNegative("new number of occurrences");
+              var desc = new PODesc.NonNegative("new number of occurrences", e.Value);
               builder.Add(Assert(GetToken(e.Value), Bpl.Expr.Le(Bpl.Expr.Literal(0), value), desc, wfOptions.AssertKv));
             } else {
               Contract.Assert(false);
@@ -536,14 +536,14 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
             if (etran.UsesOldHeap) {
               Bpl.Expr wh = GetWhereClause(e.Function.tok, etran.TrExpr(e.Function), e.Function.Type, etran, ISALLOC, true);
               if (wh != null) {
-                var desc = new PODesc.IsAllocated("function", "in the state in which the function is invoked");
+                var desc = new PODesc.IsAllocated("function", "in the state in which the function is invoked", e.Function);
                 builder.Add(Assert(GetToken(e.Function), wh, desc));
               }
               for (int i = 0; i < e.Args.Count; i++) {
                 Expression ee = e.Args[i];
                 wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran, ISALLOC, true);
                 if (wh != null) {
-                  var desc = new PODesc.IsAllocated("argument", "in the state in which the function is invoked");
+                  var desc = new PODesc.IsAllocated("argument", "in the state in which the function is invoked", ee);
                   builder.Add(Assert(GetToken(ee), wh, desc));
                 }
               }
@@ -683,7 +683,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                 if (!e.Function.IsStatic) {
                   Bpl.Expr wh = GetWhereClause(e.Receiver.tok, etran.TrExpr(e.Receiver), e.Receiver.Type, etran, ISALLOC, true);
                   if (wh != null) {
-                    var desc = new PODesc.IsAllocated("receiver argument", "in the state in which the function is invoked");
+                    var desc = new PODesc.IsAllocated("receiver argument", "in the state in which the function is invoked", e.Receiver, e.AtLabel);
                     builder.Add(Assert(GetToken(e.Receiver), wh, desc));
                   }
                 }
@@ -691,7 +691,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                   Expression ee = e.Args[i];
                   Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran, ISALLOC, true);
                   if (wh != null) {
-                    var desc = new PODesc.IsAllocated("argument", "in the state in which the function is invoked");
+                    var desc = new PODesc.IsAllocated("argument", "in the state in which the function is invoked", ee, e.AtLabel);
                     builder.Add(Assert(GetToken(ee), wh, desc));
                   }
                 }
@@ -699,7 +699,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                 if (!e.Function.IsStatic) {
                   Bpl.Expr wh = GetWhereClause(e.Receiver.tok, etran.TrExpr(e.Receiver), e.Receiver.Type, etran.OldAt(e.AtLabel), ISALLOC, true);
                   if (wh != null) {
-                    var desc = new PODesc.IsAllocated("receiver argument", "in the two-state function's previous state");
+                    var desc = new PODesc.IsAllocated("receiver argument", "in the two-state function's previous state", e.Receiver, e.AtLabel);
                     builder.Add(Assert(GetToken(e.Receiver), wh, desc));
                   }
                 }
@@ -711,10 +711,12 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                     Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(e.AtLabel), ISALLOC, true);
                     if (wh != null) {
                       var pIdx = e.Args.Count == 1 ? "" : " at index " + i;
-                      var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
-                        "in the two-state function's previous state" +
-                          PODesc.IsAllocated.HelperFormal(formal)
-                        );
+                      var desc = new PODesc.IsAllocated(
+                        $"argument{pIdx} for parameter '{formal.Name}'",
+                        "in the two-state function's previous state" + PODesc.IsAllocated.HelperFormal(formal),
+                        ee,
+                        e.AtLabel
+                      );
                       builder.Add(Assert(GetToken(ee), wh, desc));
                     }
                   }
@@ -842,7 +844,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
         case SeqConstructionExpr constructionExpr: {
             var e = constructionExpr;
             CheckWellformed(e.N, wfOptions, locals, builder, etran);
-            var desc = new PODesc.NonNegative("sequence size");
+            var desc = new PODesc.NonNegative("sequence size", e.N);
             builder.Add(Assert(GetToken(e.N), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.N)), desc));
 
             CheckWellformed(e.Initializer, wfOptions, locals, builder, etran);
@@ -876,13 +878,13 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
               } else {
                 Contract.Assert(ty.IsRefType);
                 nonNull = Bpl.Expr.Neq(r, predef.Null);
-                builder.Add(Assert(GetToken(fe.E), BplImp(ante, nonNull), new PODesc.NonNull(description, description != "object")));
+                builder.Add(Assert(GetToken(fe.E), BplImp(ante, nonNull), new PODesc.NonNull(description, fe.E, description != "object")));
               }
               // check that "r" was allocated in the "e.AtLabel" state
               Bpl.Expr wh = GetWhereClause(fe.E.tok, r, ty, etran.OldAt(e.AtLabel), ISALLOC, true);
               if (wh != null) {
                 var desc = new PODesc.IsAllocated(description, "in the old-state of the 'unchanged' predicate",
-                  description != "object");
+                  fe.E, e.AtLabel, description != "object");
                 builder.Add(Assert(GetToken(fe.E), BplImp(BplAnd(ante, nonNull), wh), desc));
               }
               // check that the 'unchanged' argument reads only what the context is allowed to read
@@ -929,22 +931,22 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                 CheckWellformed(e.E1, wfOptions, locals, builder, etran);
                 if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && e.E0.Type.IsBigOrdinalType) {
                   var rhsIsNat = FunctionCall(binaryExpr.tok, "ORD#IsNat", Bpl.Type.Bool, etran.TrExpr(e.E1));
-                  builder.Add(Assert(GetToken(expr), rhsIsNat, new PODesc.OrdinalSubtractionIsNatural()));
+                  builder.Add(Assert(GetToken(expr), rhsIsNat, new PODesc.OrdinalSubtractionIsNatural(e.E1)));
                   var offset0 = FunctionCall(binaryExpr.tok, "ORD#Offset", Bpl.Type.Int, etran.TrExpr(e.E0));
                   var offset1 = FunctionCall(binaryExpr.tok, "ORD#Offset", Bpl.Type.Int, etran.TrExpr(e.E1));
-                  builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(offset1, offset0), new PODesc.OrdinalSubtractionUnderflow()));
+                  builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(offset1, offset0), new PODesc.OrdinalSubtractionUnderflow(e.E0, e.E1)));
                 } else if (e.Type.NormalizeToAncestorType().IsCharType) {
                   var e0 = FunctionCall(binaryExpr.tok, "char#ToInt", Bpl.Type.Int, etran.TrExpr(e.E0));
                   var e1 = FunctionCall(binaryExpr.tok, "char#ToInt", Bpl.Type.Int, etran.TrExpr(e.E1));
                   if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
                     builder.Add(Assert(GetToken(expr),
                       FunctionCall(Token.NoToken, BuiltinFunction.IsChar, null,
-                        Bpl.Expr.Binary(BinaryOperator.Opcode.Add, e0, e1)), new PODesc.CharOverflow()));
+                        Bpl.Expr.Binary(BinaryOperator.Opcode.Add, e0, e1)), new PODesc.CharOverflow(e.E0, e.E1)));
                   } else {
                     Contract.Assert(e.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub);  // .Mul is not supported for char
                     builder.Add(Assert(GetToken(expr),
                       FunctionCall(Token.NoToken, BuiltinFunction.IsChar, null,
-                        Bpl.Expr.Binary(BinaryOperator.Opcode.Sub, e0, e1)), new PODesc.CharUnderflow()));
+                        Bpl.Expr.Binary(BinaryOperator.Opcode.Sub, e0, e1)), new PODesc.CharUnderflow(e.E0, e.E1)));
                   }
                 }
                 break;
@@ -966,7 +968,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
               case BinaryExpr.ResolvedOpcode.RightShift: {
                   CheckWellformed(e.E1, wfOptions, locals, builder, etran);
                   var w = e.Type.NormalizeToAncestorType().AsBitVectorType.Width;
-                  var upperDesc = new PODesc.ShiftUpperBound(w, true);
+                  var upperDesc = new PODesc.ShiftUpperBound(w, true, e.E1);
                   if (e.E1.Type.NormalizeToAncestorType().AsBitVectorType is { } bitvectorType) {
                     // Known to be non-negative, so we don't need to check lower bound.
                     // Check upper bound, that is, check "E1 <= w"
@@ -988,7 +990,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re
                       // already holds, so there is no reason to check it.
                     }
                   } else {
-                    var positiveDesc = new PODesc.ShiftLowerBound(true);
+                    var positiveDesc = new PODesc.ShiftLowerBound(true, e.E1);
                     builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(e.E1)), positiveDesc, wfOptions.AssertKv));
                     builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(etran.TrExpr(e.E1), Bpl.Expr.Literal(w)), upperDesc, wfOptions.AssertKv));
                   }
@@ -1389,8 +1391,8 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp
       if (expr.Function.Name is "RotateLeft" or "RotateRight") {
         var w = expr.Type.AsBitVectorType.Width;
         var arg = expr.Args[0];
-        builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(arg)), new PODesc.ShiftLowerBound(false), options.AssertKv));
-        builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(etran.TrExpr(arg), Bpl.Expr.Literal(w)), new PODesc.ShiftUpperBound(w, false),
+        builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(arg)), new PODesc.ShiftLowerBound(false, arg), options.AssertKv));
+        builder.Add(Assert(GetToken(expr), Bpl.Expr.Le(etran.TrExpr(arg), Bpl.Expr.Literal(w)), new PODesc.ShiftUpperBound(w, false, arg),
           options.AssertKv));
       }
     }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
index 0fe86915b1..d9df416cc3 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
@@ -140,7 +140,7 @@ void AddWellformednessCheck(Function f) {
         if (formal.IsOld) {
           Bpl.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
           if (wh != null) {
-            var desc = new PODesc.IsAllocated("default value", "in the two-state function's previous state");
+            var desc = new PODesc.IsAllocated("default value", "in the two-state function's previous state", e);
             builder.Add(Assert(GetToken(e), wh, desc));
           }
         }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index 8f03c2cbc5..00e84407a1 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -689,7 +689,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP
             if (formal.IsOld) {
               Boogie.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true);
               if (wh != null) {
-                var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state");
+                var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state", e);
                 builder.Add(Assert(e.RangeToken, wh, desc));
               }
             }
@@ -1671,8 +1671,9 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal);
             var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
             var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
-              "in the two-state lemma's previous state" +
-              PODesc.IsAllocated.HelperFormal(formal));
+              "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal),
+              dafnyFormalIdExpr
+            );
             var require = Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
               desc.FailureDescription, desc.SuccessDescription, null);
             require.Description = desc;
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
index 2ea293d351..f377d7afd7 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
@@ -921,7 +921,7 @@ private void TrForLoop(ForLoopStmt stmt, BoogieStmtListBuilder builder, List<Var
 
       // check lo <= hi
       if (lo != null && hi != null) {
-        builder.Add(Assert(lo.tok, Bpl.Expr.Le(bLo, bHi), new PODesc.ForRangeBoundsValid()));
+        builder.Add(Assert(lo.tok, Bpl.Expr.Le(bLo, bHi), new PODesc.ForRangeBoundsValid(lo, hi)));
       }
       // check forall x :: lo <= x <= hi ==> Is(x, typ)
       {
@@ -939,7 +939,20 @@ private void TrForLoop(ForLoopStmt stmt, BoogieStmtListBuilder builder, List<Var
           locals.Add(xVar);
           builder.Add(new Bpl.HavocCmd(tok, new List<Bpl.IdentifierExpr>() { x }));
           builder.Add(new Bpl.AssumeCmd(tok, ForLoopBounds(x, bLo, bHi)));
-          builder.Add(Assert(tok, cre, new PODesc.ForRangeAssignable(desc)));
+          List<Expression> dafnyRangeBounds = new();
+          if (lo != null) {
+            dafnyRangeBounds.Add(new BinaryExpr(stmt.tok, BinaryExpr.Opcode.Le, lo, dIndex));
+          }
+          if (hi != null) {
+            dafnyRangeBounds.Add(new BinaryExpr(stmt.tok, BinaryExpr.Opcode.Le, dIndex, hi));
+          }
+
+          Expression dafnyRange = dafnyRangeBounds.Count == 1
+            ? dafnyRangeBounds[0]
+            : new BinaryExpr(stmt.tok, BinaryExpr.Opcode.And, dafnyRangeBounds[0], dafnyRangeBounds[1]);
+          var dafnyAssertion = new ForallExpr(stmt.tok, stmt.RangeToken, new List<BoundVar> { indexVar },
+            dafnyRange, new TypeTestExpr(indexVar.tok, dIndex, indexVar.Type), null);
+          builder.Add(Assert(tok, cre, new PODesc.ForRangeAssignable(desc, dafnyAssertion)));
         }
       }
 
@@ -1100,7 +1113,7 @@ void TrForallProof(ForallStmt s, BoogieStmtListBuilder definedness, BoogieStmtLi
         foreach (var ens in s.Ens) {
           foreach (var split in TrSplitExpr(ens.E, etran, true, out var splitHappened)) {
             if (split.IsChecked) {
-              definedness.Add(Assert(split.Tok, split.E, new PODesc.ForallPostcondition()));
+              definedness.Add(Assert(split.Tok, split.E, new PODesc.ForallPostcondition(ens.E)));
             }
           }
         }
@@ -1911,7 +1924,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         if (!method.IsStatic && !(method is Constructor)) {
           Bpl.Expr wh = GetWhereClause(receiver.tok, etran.TrExpr(receiver), receiver.Type, etran, ISALLOC, true);
           if (wh != null) {
-            var desc = new PODesc.IsAllocated("receiver argument", "in the state in which the method is invoked");
+            var desc = new PODesc.IsAllocated("receiver argument", "in the state in which the method is invoked", receiver);
             builder.Add(Assert(receiver.tok, wh, desc));
           }
         }
@@ -1919,7 +1932,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
           Expression ee = Args[i];
           Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran, ISALLOC, true);
           if (wh != null) {
-            var desc = new PODesc.IsAllocated("argument", "in the state in which the method is invoked");
+            var desc = new PODesc.IsAllocated("argument", "in the state in which the method is invoked", ee);
             builder.Add(Assert(ee.tok, wh, desc));
           }
         }
@@ -1927,7 +1940,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         if (!method.IsStatic) {
           Bpl.Expr wh = GetWhereClause(receiver.tok, etran.TrExpr(receiver), receiver.Type, etran.OldAt(atLabel), ISALLOC, true);
           if (wh != null) {
-            var desc = new PODesc.IsAllocated("receiver argument", "in the two-state lemma's previous state");
+            var desc = new PODesc.IsAllocated("receiver argument", "in the two-state lemma's previous state", receiver, atLabel);
             builder.Add(Assert(receiver.tok, wh, desc));
           }
         }
@@ -1939,10 +1952,12 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
             Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran.OldAt(atLabel), ISALLOC, true);
             if (wh != null) {
               var pIdx = Args.Count == 1 ? "" : " at index " + i;
-              var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
-                "in the two-state lemma's previous state" +
-                PODesc.IsAllocated.HelperFormal(formal)
-                );
+              var desc = new PODesc.IsAllocated(
+                $"argument{pIdx} for parameter '{formal.Name}'",
+                "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal),
+                ee,
+                atLabel
+              );
               builder.Add(Assert(ee.tok, wh, desc));
             }
           }
@@ -2648,7 +2663,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs
           foreach (Expression dim in tRhs.ArrayDimensions) {
             CheckWellformed(dim, new WFOptions(), locals, builder, etran);
             var desc = new PODesc.NonNegative(tRhs.ArrayDimensions.Count == 1
-              ? "array size" : $"array size (dimension {i})");
+              ? "array size" : $"array size (dimension {i})", dim);
             builder.Add(Assert(GetToken(dim), Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(dim)), desc));
             i++;
           }
@@ -2656,7 +2671,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs
             CheckWellformed(tRhs.ElementInit, new WFOptions(), locals, builder, etran);
           } else if (tRhs.InitDisplay != null) {
             var dim = tRhs.ArrayDimensions[0];
-            var desc = new PODesc.ArrayInitSizeValid(tRhs.InitDisplay.Count);
+            var desc = new PODesc.ArrayInitSizeValid(tRhs, dim);
             builder.Add(Assert(GetToken(dim), Bpl.Expr.Eq(etran.TrExpr(dim), Bpl.Expr.Literal(tRhs.InitDisplay.Count)), desc));
             foreach (var v in tRhs.InitDisplay) {
               CheckWellformed(v, new WFOptions(), locals, builder, etran);
@@ -2671,7 +2686,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs
             foreach (Expression dim in tRhs.ArrayDimensions) {
               zeroSize = BplOr(zeroSize, Bpl.Expr.Eq(Bpl.Expr.Literal(0), etran.TrExpr(dim)));
             }
-            var desc = new PODesc.ArrayInitEmpty(tRhs.EType.ToString());
+            var desc = new PODesc.ArrayInitEmpty(tRhs.EType.ToString(), tRhs.ArrayDimensions);
             builder.Add(Assert(tRhs.Tok, zeroSize, desc));
           }
         }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
index b144cbeb2f..8d80f53220 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
@@ -1223,19 +1223,21 @@ void PutSourceIntoLocal() {
       Bpl.Expr from = FunctionCall(tok, BuiltinFunction.RealToInt, null, o);
       Bpl.Expr e = FunctionCall(tok, BuiltinFunction.IntToReal, null, from);
       e = Bpl.Expr.Binary(tok, Bpl.BinaryOperator.Opcode.Eq, e, o);
-      builder.Add(Assert(tok, e, new PODesc.IsInteger(errorMsgPrefix)));
+      builder.Add(Assert(tok, e, new PODesc.IsInteger(expr, errorMsgPrefix)));
     }
 
     if (fromType.IsBigOrdinalType && !toType.IsBigOrdinalType) {
       PutSourceIntoLocal();
       Bpl.Expr boundsCheck = FunctionCall(tok, "ORD#IsNat", Bpl.Type.Bool, o);
-      builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionIsNatural(errorMsgPrefix)));
+      builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionIsNatural(errorMsgPrefix, expr)));
     }
 
     if (toTypeFamily.IsBitVectorType) {
       var toWidth = toTypeFamily.AsBitVectorType.Width;
       var toBound = BaseTypes.BigNum.FromBigInt(BigInteger.One << toWidth);  // 1 << toWidth
       Bpl.Expr boundsCheck = null;
+      var dafnyBound = new BinaryExpr(expr.tok, BinaryExpr.Opcode.LeftShift, Expression.CreateIntLiteral(expr.tok, 1), Expression.CreateIntLiteral(expr.tok, toWidth));
+      Expression dafnyBoundsCheck = null;
       if (fromTypeFamily.IsBitVectorType) {
         var fromWidth = fromTypeFamily.AsBitVectorType.Width;
         if (toWidth < fromWidth) {
@@ -1243,38 +1245,58 @@ void PutSourceIntoLocal() {
           PutSourceIntoLocal();
           var bound = BplBvLiteralExpr(tok, toBound, fromTypeFamily.AsBitVectorType);
           boundsCheck = FunctionCall(expr.tok, "lt_bv" + fromWidth, Bpl.Type.Bool, o, bound);
+          dafnyBoundsCheck = new BinaryExpr(expr.tok, BinaryExpr.Opcode.And,
+            new BinaryExpr(expr.tok, BinaryExpr.Opcode.Le, new LiteralExpr(expr.tok, 0), expr),
+            new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, dafnyBound)
+        );
         }
       } else if (fromType.IsNumericBased(Type.NumericPersuasion.Int) || fromTypeFamily.IsCharType) {
-        // Check "expr < (1 << toWdith)" in type "int"
+        // Check "expr < (1 << toWidth)" in type "int"
         PutSourceIntoLocal();
         var bound = Bpl.Expr.Literal(toBound);
         boundsCheck = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), o), Bpl.Expr.Lt(o, bound));
+        dafnyBoundsCheck = Expression.CreateAnd(
+          Expression.CreateLess(Expression.CreateIntLiteral(expr.tok, 0), expr),
+          Expression.CreateAtMost(expr, dafnyBound));
       } else if (fromType.IsNumericBased(Type.NumericPersuasion.Real)) {
-        // Check "Int(expr) < (1 << toWdith)" in type "int"
+        // Check "Int(expr) < (1 << toWidth)" in type "int"
         PutSourceIntoLocal();
         var bound = Bpl.Expr.Literal(toBound);
         var oi = FunctionCall(tok, BuiltinFunction.RealToInt, null, o);
         boundsCheck = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), oi), Bpl.Expr.Lt(oi, bound));
+        var intExpr = new ExprDotName(expr.tok, expr, "Floor", null);
+        dafnyBoundsCheck = new BinaryExpr(expr.tok, BinaryExpr.Opcode.And,
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Le, new LiteralExpr(expr.tok, 0), intExpr),
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, intExpr, dafnyBound)
+        );
       } else if (fromType.IsBigOrdinalType) {
         var bound = Bpl.Expr.Literal(toBound);
         var oi = FunctionCall(tok, "ORD#Offset", Bpl.Type.Int, o);
         boundsCheck = Bpl.Expr.Lt(oi, bound);
+        var intExpr = new ExprDotName(expr.tok, expr, "Offset", null);
+        dafnyBoundsCheck = new BinaryExpr(expr.tok, BinaryExpr.Opcode.And,
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Le, new LiteralExpr(expr.tok, 0), intExpr),
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, intExpr, dafnyBound)
+        );
       }
 
       if (boundsCheck != null) {
-        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, errorMsgPrefix)));
+        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, dafnyBoundsCheck, errorMsgPrefix)));
       }
 
     } else if (toType.IsCharType) {
       if (fromType.IsNumericBased(Type.NumericPersuasion.Int)) {
         PutSourceIntoLocal();
         var boundsCheck = FunctionCall(Token.NoToken, BuiltinFunction.IsChar, null, o);
-        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, errorMsgPrefix)));
+        var dafnyBoundsCheck = PODesc.Utils.MakeCharBoundsCheck(options, expr);
+        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, dafnyBoundsCheck, errorMsgPrefix)));
       } else if (fromType.IsNumericBased(Type.NumericPersuasion.Real)) {
         PutSourceIntoLocal();
         var oi = FunctionCall(tok, BuiltinFunction.RealToInt, null, o);
         var boundsCheck = FunctionCall(Token.NoToken, BuiltinFunction.IsChar, null, oi);
-        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("real value", toType, errorMsgPrefix)));
+        Expression intExpr = new ExprDotName(expr.tok, expr, "Floor", null);
+        var dafnyBoundsCheck = PODesc.Utils.MakeCharBoundsCheck(options, intExpr);
+        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("real value", toType, dafnyBoundsCheck, errorMsgPrefix)));
       } else if (fromType.IsBitVectorType) {
         PutSourceIntoLocal();
         var fromWidth = fromType.AsBitVectorType.Width;
@@ -1285,7 +1307,9 @@ void PutSourceIntoLocal() {
           var toBound = BaseTypes.BigNum.FromBigInt(BigInteger.One << toWidth); // 1 << toWidth
           var bound = BplBvLiteralExpr(tok, toBound, fromType.AsBitVectorType);
           var boundsCheck = FunctionCall(expr.tok, "lt_bv" + fromWidth, Bpl.Type.Bool, o, bound);
-          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("bit-vector value", toType, errorMsgPrefix)));
+          var dafnyBound = new BinaryExpr(expr.tok, BinaryExpr.Opcode.LeftShift, Expression.CreateIntLiteral(expr.tok, 1), Expression.CreateIntLiteral(expr.tok, toWidth));
+          var dafnyBoundsCheck = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, dafnyBound);
+          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("bit-vector value", toType, dafnyBoundsCheck, errorMsgPrefix)));
         }
       } else if (fromType.IsBigOrdinalType) {
         PutSourceIntoLocal();
@@ -1294,21 +1318,25 @@ void PutSourceIntoLocal() {
         var toBound = BaseTypes.BigNum.FromBigInt(BigInteger.One << toWidth); // 1 << toWidth
         var bound = Bpl.Expr.Literal(toBound);
         var boundsCheck = Bpl.Expr.Lt(oi, bound);
-        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("ORDINAL value", toType, errorMsgPrefix)));
+        var dafnyBound = new BinaryExpr(expr.tok, BinaryExpr.Opcode.LeftShift, Expression.CreateIntLiteral(expr.tok, 1), Expression.CreateIntLiteral(expr.tok, toWidth));
+        var offset = new ExprDotName(expr.tok, expr, "Offset", null);
+        var dafnyBoundsCheck = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, offset, dafnyBound);
+        builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("ORDINAL value", toType, dafnyBoundsCheck, errorMsgPrefix)));
       }
 
     } else if (toType.IsBigOrdinalType) {
       if (fromType.IsNumericBased(Type.NumericPersuasion.Int)) {
         PutSourceIntoLocal();
         Bpl.Expr boundsCheck = Bpl.Expr.Le(Bpl.Expr.Literal(0), o);
-        var desc = new PODesc.ConversionPositive("integer", toType, errorMsgPrefix);
+        var desc = new PODesc.ConversionPositive("integer", toType, expr, errorMsgPrefix);
         builder.Add(Assert(tok, boundsCheck, desc));
       }
       if (fromType.IsNumericBased(Type.NumericPersuasion.Real)) {
         PutSourceIntoLocal();
         var oi = FunctionCall(tok, BuiltinFunction.RealToInt, null, o);
         Bpl.Expr boundsCheck = Bpl.Expr.Le(Bpl.Expr.Literal(0), oi);
-        var desc = new PODesc.ConversionPositive("real", toType, errorMsgPrefix);
+        var intExpr = new ExprDotName(expr.tok, expr, "Floor", null);
+        var desc = new PODesc.ConversionPositive("real", toType, intExpr, errorMsgPrefix);
         builder.Add(Assert(tok, boundsCheck, desc));
       }
 
@@ -1331,13 +1359,14 @@ void PutSourceIntoLocal() {
       } else {
         be = o;
       }
-      CheckResultToBeInType_Aux(tok, new BoogieWrapper(be, toTypeFamily), toType.NormalizeExpandKeepConstraints(), builder, etran, errorMsgPrefix);
+      CheckResultToBeInType_Aux(tok, new BoogieWrapper(be, toTypeFamily), expr, toType.NormalizeExpandKeepConstraints(), builder, etran, errorMsgPrefix);
     }
   }
 
-  void CheckResultToBeInType_Aux(IToken tok, Expression expr, Type toType, BoogieStmtListBuilder builder, ExpressionTranslator etran, string errorMsgPrefix) {
+  void CheckResultToBeInType_Aux(IToken tok, Expression boogieExpr, Expression origExpr, Type toType, BoogieStmtListBuilder builder, ExpressionTranslator etran, string errorMsgPrefix) {
     Contract.Requires(tok != null);
-    Contract.Requires(expr != null);
+    Contract.Requires(boogieExpr != null);
+    Contract.Requires(origExpr != null);
     Contract.Requires(toType != null && toType.AsRedirectingType != null);
     Contract.Requires(builder != null);
     Contract.Requires(etran != null);
@@ -1359,16 +1388,15 @@ void CheckResultToBeInType_Aux(IToken tok, Expression expr, Type toType, BoogieS
     }
 
     if (baseType.AsRedirectingType != null) {
-      CheckResultToBeInType_Aux(tok, expr, baseType, builder, etran, errorMsgPrefix);
+      CheckResultToBeInType_Aux(tok, boogieExpr, origExpr, baseType, builder, etran, errorMsgPrefix);
     }
     // Check any constraint defined in 'dd'
     if (rdt.Var != null) {
       // TODO: use TrSplitExpr
-      var substMap = new Dictionary<IVariable, Expression>();
-      substMap.Add(rdt.Var, expr);
       var typeMap = TypeParameter.SubstitutionMap(rdt.TypeArgs, udt.TypeArgs);
-      var constraint = etran.TrExpr(Substitute(rdt.Constraint, null, substMap, typeMap));
-      builder.Add(Assert(tok, constraint, new PODesc.ConversionSatisfiesConstraints(errorMsgPrefix, kind, rdt.Name)));
+      var dafnyConstraint = Substitute(rdt.Constraint, null, new() { { rdt.Var, origExpr } }, typeMap);
+      var boogieConstraint = etran.TrExpr(Substitute(rdt.Constraint, null, new() { { rdt.Var, boogieExpr } }, typeMap));
+      builder.Add(Assert(tok, boogieConstraint, new PODesc.ConversionSatisfiesConstraints(errorMsgPrefix, kind, rdt.Name, dafnyConstraint)));
     }
   }
 
@@ -1491,7 +1519,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) {
 
       bool splitHappened;
       var ss = TrSplitExpr(witnessExpr, etran, true, out splitHappened);
-      var desc = new PODesc.WitnessCheck(witnessString);
+      var desc = new PODesc.WitnessCheck(witnessString, witnessExpr);
       if (!splitHappened) {
         witnessCheckBuilder.Add(Assert(witnessCheckTok, etran.TrExpr(witnessExpr), desc));
       } else {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
index 115116be89..c3d7cfad95 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -2530,7 +2530,7 @@ void CheckNonNull(IToken tok, Expression e, BoogieStmtListBuilder builder, Expre
       } else if (e is StaticReceiverExpr) {
         // also ok
       } else {
-        builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), new PODesc.NonNull("target object"), kv));
+        builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), new PODesc.NonNull("target object", e), kv));
       }
     }
 
diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs
index eeb61c4999..c48f11ffb4 100644
--- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs
+++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs
@@ -1,7 +1,9 @@
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using System.Linq.Expressions;
 using JetBrains.Annotations;
 using Microsoft.Boogie;
 
@@ -50,9 +52,11 @@ public override Expression GetAssertedExpr(DafnyOptions options) {
 
 public abstract class ShiftOrRotateBound : ProofObligationDescription {
   protected readonly string shiftOrRotate;
+  protected readonly Expression amount;
 
-  public ShiftOrRotateBound(bool shift) {
+  public ShiftOrRotateBound(bool shift, Expression amount) {
     shiftOrRotate = shift ? "shift" : "rotate";
+    this.amount = amount;
   }
 }
 
@@ -65,8 +69,12 @@ public class ShiftLowerBound : ShiftOrRotateBound {
 
   public override string ShortDescription => $"{shiftOrRotate} lower bound";
 
-  public ShiftLowerBound(bool shift)
-    : base(shift) {
+  public ShiftLowerBound(bool shift, Expression amount)
+    : base(shift, amount) {
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(amount.tok, BinaryExpr.Opcode.Le, Expression.CreateIntLiteral(amount.tok, 0), amount);
   }
 }
 
@@ -81,10 +89,14 @@ public class ShiftUpperBound : ShiftOrRotateBound {
 
   private readonly int width;
 
-  public ShiftUpperBound(int width, bool shift)
-    : base(shift) {
+  public ShiftUpperBound(int width, bool shift, Expression amount)
+    : base(shift, amount) {
     this.width = width;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(amount.tok, BinaryExpr.Opcode.Le, amount, Expression.CreateIntLiteral(amount.tok, width));
+  }
 }
 
 public class ConversionIsNatural : ProofObligationDescription {
@@ -97,9 +109,15 @@ public class ConversionIsNatural : ProofObligationDescription {
   public override string ShortDescription => "converted value is natural";
 
   private readonly string prefix;
+  private readonly Expression value;
 
-  public ConversionIsNatural(string prefix) {
+  public ConversionIsNatural(string prefix, Expression value) {
     this.prefix = prefix;
+    this.value = value;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new TypeTestExpr(value.tok, value, Type.Nat());
   }
 }
 
@@ -115,11 +133,17 @@ public class ConversionSatisfiesConstraints : ProofObligationDescription {
   private readonly string prefix;
   private readonly string kind;
   private readonly string name;
+  private readonly Expression constraint;
 
-  public ConversionSatisfiesConstraints(string prefix, string kind, string name) {
+  public ConversionSatisfiesConstraints(string prefix, string kind, string name, Expression constraint) {
     this.prefix = prefix;
     this.kind = kind;
     this.name = name;
+    this.constraint = constraint;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return constraint;
   }
 }
 
@@ -131,6 +155,16 @@ public class OrdinalSubtractionIsNatural : ProofObligationDescription {
     "RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger";
 
   public override string ShortDescription => "ordinal subtraction is natural";
+
+  private readonly Expression rhs;
+
+  public OrdinalSubtractionIsNatural(Expression rhs) {
+    this.rhs = rhs;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new ExprDotName(rhs.tok, rhs, "IsNat", null);
+  }
 }
 
 public class OrdinalSubtractionUnderflow : ProofObligationDescription {
@@ -141,6 +175,23 @@ public class OrdinalSubtractionUnderflow : ProofObligationDescription {
     "ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)";
 
   public override string ShortDescription => "ordinal subtraction underflow";
+
+  private readonly Expression lhs;
+  private readonly Expression rhs;
+
+  public OrdinalSubtractionUnderflow(Expression lhs, Expression rhs) {
+    this.lhs = lhs;
+    this.rhs = rhs;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(
+      rhs.tok,
+      BinaryExpr.Opcode.Le,
+      new ExprDotName(rhs.tok, rhs, "Offset", null),
+      new ExprDotName(lhs.tok, lhs, "Offset", null)
+    );
+  }
 }
 
 public class CharOverflow : ProofObligationDescription {
@@ -151,6 +202,24 @@ public class CharOverflow : ProofObligationDescription {
     "char addition might overflow";
 
   public override string ShortDescription => "char overflow";
+
+  private readonly Expression e0;
+  private readonly Expression e1;
+
+  public CharOverflow(Expression e0, Expression e1) {
+    this.e0 = e0;
+    this.e1 = e1;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    var sum = new BinaryExpr(
+      e0.tok,
+      BinaryExpr.Opcode.Add,
+      new ConversionExpr(e0.tok, e0, Type.Int),
+      new ConversionExpr(e1.tok, e1, Type.Int)
+    );
+    return Utils.MakeCharBoundsCheck(options, sum);
+  }
 }
 
 public class CharUnderflow : ProofObligationDescription {
@@ -161,6 +230,24 @@ public class CharUnderflow : ProofObligationDescription {
     "char subtraction might underflow";
 
   public override string ShortDescription => "char underflow";
+
+  private readonly Expression e0;
+  private readonly Expression e1;
+
+  public CharUnderflow(Expression e0, Expression e1) {
+    this.e0 = e0;
+    this.e1 = e1;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    var diff = new BinaryExpr(
+      e0.tok,
+      BinaryExpr.Opcode.Sub,
+      new ConversionExpr(e0.tok, e0, Type.Int),
+      new ConversionExpr(e1.tok, e1, Type.Int)
+    );
+    return Utils.MakeCharBoundsCheck(options, diff);
+  }
 }
 
 public class ConversionFit : ProofObligationDescription {
@@ -175,12 +262,18 @@ public class ConversionFit : ProofObligationDescription {
   private readonly string prefix;
   private readonly string what;
   private readonly Type toType;
+  private readonly Expression boundsCheck;
 
-  public ConversionFit(string what, Type toType, string prefix = "") {
+  public ConversionFit(string what, Type toType, Expression boundsCheck, string prefix = "") {
     this.prefix = prefix;
     this.what = what;
+    this.boundsCheck = boundsCheck;
     this.toType = toType;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return boundsCheck;
+  }
 }
 
 public class NonNegative : ProofObligationDescription {
@@ -193,9 +286,20 @@ public class NonNegative : ProofObligationDescription {
   public override string ShortDescription => "non-negative";
 
   private readonly string what;
+  private readonly Expression expr;
 
-  public NonNegative(string what) {
+  public NonNegative(string what, Expression expr) {
     this.what = what;
+    this.expr = expr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.Le,
+      Expression.CreateIntLiteral(expr.tok, 0),
+      expr
+    );
   }
 }
 
@@ -211,11 +315,22 @@ public class ConversionPositive : ProofObligationDescription {
   private readonly string prefix;
   private readonly string what;
   private readonly Type toType;
+  private readonly Expression expr;
 
-  public ConversionPositive(string what, Type toType, string prefix = "") {
+  public ConversionPositive(string what, Type toType, Expression expr, string prefix = "") {
     this.prefix = prefix;
     this.what = what;
     this.toType = toType;
+    this.expr = expr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.Le,
+      Expression.CreateIntLiteral(expr.tok, 0),
+      expr
+    );
   }
 }
 
@@ -229,10 +344,21 @@ public class IsInteger : ProofObligationDescription {
   public override string ShortDescription => "is integer";
 
   private readonly string prefix;
+  private readonly Expression expr;
 
-  public IsInteger(string prefix = "") {
+  public IsInteger(Expression expr, string prefix = "") {
+    this.expr = expr;
     this.prefix = prefix;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.Eq,
+      expr,
+      new ConversionExpr(expr.tok, new ExprDotName(expr.tok, expr, "Floor", null), Type.Real)
+    );
+  }
 }
 
 //// Object properties
@@ -246,14 +372,20 @@ public class NonNull : ProofObligationDescription {
 
   public override string ShortDescription => $"{what} non-null";
   private readonly string what;
+  private readonly Expression expr;
   private bool plural;
   private string PluralSuccess => plural ? "each " : "";
   private string PluralFailure => plural ? "some " : "";
 
-  public NonNull(string what, bool plural = false) {
+  public NonNull(string what, Expression expr, bool plural = false) {
     this.what = what;
+    this.expr = expr;
     this.plural = plural;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(expr.tok, BinaryExpr.Opcode.Neq, expr, new LiteralExpr(expr.tok));
+  }
 }
 
 public class IsAllocated : ProofObligationDescription {
@@ -267,6 +399,8 @@ public class IsAllocated : ProofObligationDescription {
 
   private readonly string what;
   [CanBeNull] private readonly string when;
+  private readonly Expression expr;
+  [CanBeNull] private readonly Label atLabel;
   private bool plural;
   private string WhenSuffix => when is null ? "" : $" {when}";
   private string PluralSuccess => plural ? "each " : "";
@@ -277,11 +411,17 @@ public static string HelperFormal(Formal formal) {
            + " arguments can refer to expressions possibly unallocated in the previous state";
   }
 
-  public IsAllocated(string what, string when, bool plural = false) {
+  public IsAllocated(string what, string when, Expression expr, [CanBeNull] Label atLabel = null, bool plural = false) {
     this.what = what;
     this.when = when;
+    this.expr = expr;
+    this.atLabel = atLabel;
     this.plural = plural;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new OldExpr(expr.tok, new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Allocated, expr), atLabel?.Name);
+  }
 }
 
 public class IsOlderProofObligation : ProofObligationDescription {
@@ -474,6 +614,16 @@ public class ForallPostcondition : ProofObligationDescription {
     "possible violation of postcondition of forall statement";
 
   public override string ShortDescription => "forall ensures";
+
+  private readonly Expression expr;
+
+  public ForallPostcondition(Expression expr) {
+    this.expr = expr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return expr;
+  }
 }
 
 public class YieldEnsures : ProofObligationDescription {
@@ -882,9 +1032,15 @@ witnessString is null
   private readonly string hintMsg =
     "; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type";
   private readonly string witnessString;
+  [CanBeNull] private readonly Expression witnessExpr;
 
-  public WitnessCheck(string witnessString) {
+  public WitnessCheck(string witnessString, Expression witnessExpr = null) {
     this.witnessString = witnessString;
+    this.witnessExpr = witnessExpr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return witnessExpr ?? base.GetAssertedExpr(options);
   }
 }
 
@@ -906,6 +1062,18 @@ public class ForRangeBoundsValid : ProofObligationDescription {
     "lower bound must not exceed upper bound";
 
   public override string ShortDescription => "for range bounds";
+
+  private readonly Expression lo;
+  private readonly Expression hi;
+
+  public ForRangeBoundsValid(Expression lo, Expression hi) {
+    this.lo = lo;
+    this.hi = hi;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(lo.tok, BinaryExpr.Opcode.Le, lo, hi);
+  }
 }
 
 public class ForRangeAssignable : ProofObligationDescription {
@@ -918,9 +1086,15 @@ public class ForRangeAssignable : ProofObligationDescription {
   public override string ShortDescription => "for range assignable";
 
   private readonly ProofObligationDescription desc;
+  private readonly Expression expr;
 
-  public ForRangeAssignable(ProofObligationDescription desc) {
+  public ForRangeAssignable(ProofObligationDescription desc, Expression expr) {
     this.desc = desc;
+    this.expr = expr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return expr;
   }
 }
 
@@ -1123,10 +1297,18 @@ public class ArrayInitSizeValid : ProofObligationDescription {
 
   public override string ShortDescription => "array initializer size";
 
-  private readonly int size;
+  private readonly TypeRhs rhs;
+  private readonly Expression dim;
+  private int size => rhs.InitDisplay.Count;
+
+  public ArrayInitSizeValid(TypeRhs rhs, Expression dim) {
+    this.rhs = rhs;
+    this.dim = dim;
+  }
 
-  public ArrayInitSizeValid(int size) {
-    this.size = size;
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    var initDisplaySize = new UnaryOpExpr(rhs.tok, UnaryOpExpr.Opcode.Cardinality, new SeqDisplayExpr(rhs.tok, rhs.InitDisplay));
+    return new BinaryExpr(dim.tok, BinaryExpr.Opcode.Eq, dim, initDisplaySize);
   }
 }
 
@@ -1140,9 +1322,25 @@ public class ArrayInitEmpty : ProofObligationDescription {
   public override string ShortDescription => "array initializer empty";
 
   private readonly string typeDesc;
+  private readonly ImmutableList<Expression> dims;
 
-  public ArrayInitEmpty(string typeDesc) {
+  public ArrayInitEmpty(string typeDesc, List<Expression> dims) {
     this.typeDesc = typeDesc;
+    this.dims = dims.ToImmutableList();
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    Expression zero = Expression.CreateIntLiteral(dims[0].tok, 0);
+    Expression zeroSize = new BinaryExpr(dims[0].tok, BinaryExpr.Opcode.Eq, dims[0], zero);
+    foreach (Expression dim in dims.Skip(1)) {
+      zeroSize = new BinaryExpr(
+        dim.tok,
+        BinaryExpr.Opcode.Or,
+        zeroSize,
+        new BinaryExpr(dim.tok, BinaryExpr.Opcode.Eq, dim, zero)
+      );
+    }
+    return zeroSize;
   }
 }
 
@@ -1253,3 +1451,38 @@ public BoilerplateTriple(string errorMessage, string successMessage, string comm
     this.DefaultFailureDescription = comment;
   }
 }
+
+internal class Utils {
+  public static Expression MakeCharBoundsCheck(DafnyOptions options, Expression expr) {
+    return options.Get(CommonOptionBag.UnicodeCharacters)
+      ? MakeCharBoundsCheckUnicode(expr)
+      : MakeCharBoundsCheckNonUnicode(expr);
+  }
+
+  public static Expression MakeCharBoundsCheckNonUnicode(Expression expr) {
+    return new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.And,
+      new BinaryExpr(
+        expr.tok, BinaryExpr.Opcode.Le, Expression.CreateIntLiteral(Token.NoToken, 0), expr),
+      new BinaryExpr(
+        expr.tok, BinaryExpr.Opcode.Lt, expr, Expression.CreateIntLiteral(expr.tok, 0x1_0000))
+    );
+  }
+
+  public static Expression MakeCharBoundsCheckUnicode(Expression expr) {
+    Expression lowRange = new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.And,
+      new BinaryExpr(expr.tok, BinaryExpr.Opcode.Le, Expression.CreateIntLiteral(Token.NoToken, 0), expr),
+      new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, Expression.CreateIntLiteral(expr.tok, 0xD800))
+    );
+    Expression highRange = new BinaryExpr(
+      expr.tok,
+      BinaryExpr.Opcode.And,
+      new BinaryExpr(expr.tok, BinaryExpr.Opcode.Le, Expression.CreateIntLiteral(Token.NoToken, 0xE000), expr),
+      new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, Expression.CreateIntLiteral(expr.tok, 0x11_0000))
+    );
+    return new BinaryExpr(lowRange.tok, BinaryExpr.Opcode.Or, lowRange, highRange);
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy
new file mode 100644
index 0000000000..ca7e77f42f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method ArrayInitEmpty<T>() {
+    var a := new T[1];
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect
new file mode 100644
index 0000000000..a5417cc8f5
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-empty.dfy.expect
@@ -0,0 +1,4 @@
+array-init-empty.dfy(5,13): Error: unless an initializer is provided for the array elements, a new array of 'T' must have empty size
+ Asserted expression: 1 == 0
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy
new file mode 100644
index 0000000000..b31dea25ca
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method ArrayInitSizeValid() {
+    var a := new int[1] [];
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect
new file mode 100644
index 0000000000..9b0c38f7c8
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/array-init-size-valid.dfy.expect
@@ -0,0 +1,4 @@
+array-init-size-valid.dfy(5,21): Error: given array size must agree with the number of expressions in the initializing display (0)
+ Asserted expression: 1 == |[]|
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy
new file mode 100644
index 0000000000..67a9c494f9
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function CanOverflow(c0: char, c1: char): char {
+    c0 + c1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect
new file mode 100644
index 0000000000..31fd0758ef
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-non-unicode.dfy.expect
@@ -0,0 +1,5 @@
+CLI: Warning: the option unicode-char has been deprecated.
+char-overflow-non-unicode.dfy(5,7): Error: char addition might overflow
+ Asserted expression: 0 <= c0 as int + c1 as int && c0 as int + c1 as int < 65536
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy
new file mode 100644
index 0000000000..322ce3f0ea
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function CanOverflow(c0: char, c1: char): char {
+    c0 + c1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect
new file mode 100644
index 0000000000..84ced7e07c
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-overflow-unicode.dfy.expect
@@ -0,0 +1,4 @@
+char-overflow-unicode.dfy(5,7): Error: char addition might overflow
+ Asserted expression: (0 <= c0 as int + c1 as int && c0 as int + c1 as int < 55296) || (57344 <= c0 as int + c1 as int && c0 as int + c1 as int < 1114112)
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy
new file mode 100644
index 0000000000..be48ec8535
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --unicode-char=false --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function CanUnderflow(c0: char, c1: char): char {
+    c0 - c1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect
new file mode 100644
index 0000000000..3d8b7954c0
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-non-unicode.dfy.expect
@@ -0,0 +1,5 @@
+CLI: Warning: the option unicode-char has been deprecated.
+char-underflow-non-unicode.dfy(5,7): Error: char subtraction might underflow
+ Asserted expression: 0 <= c0 as int - c1 as int && c0 as int - c1 as int < 65536
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy
new file mode 100644
index 0000000000..f24d042b5f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function CanUnderflow(c0: char, c1: char): char {
+    c0 - c1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect
new file mode 100644
index 0000000000..cd323ff824
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/char-underflow-unicode.dfy.expect
@@ -0,0 +1,4 @@
+char-underflow-unicode.dfy(5,7): Error: char subtraction might underflow
+ Asserted expression: (0 <= c0 as int - c1 as int && c0 as int - c1 as int < 55296) || (57344 <= c0 as int - c1 as int && c0 as int - c1 as int < 1114112)
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy
new file mode 100644
index 0000000000..22354e6c09
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function ConversionFit(i: int): bv8
+{
+    i as bv8
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect
new file mode 100644
index 0000000000..ff47748b7b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-fit.dfy.expect
@@ -0,0 +1,4 @@
+conversion-fit.dfy(6,6): Error: value to be converted might not fit in bv8
+ Asserted expression: 0 < i && i <= 1 << 8
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy
new file mode 100644
index 0000000000..fe73c1edf4
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function ConversionIsNatural(ord: ORDINAL): int
+{
+    ord as int
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect
new file mode 100644
index 0000000000..641f55a5cd
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-is-natural.dfy.expect
@@ -0,0 +1,4 @@
+conversion-is-natural.dfy(6,8): Error: value to be converted might be bigger than every natural number
+ Asserted expression: ord is nat
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy
new file mode 100644
index 0000000000..7388fe8f59
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function ConversionPositive(i: int): ORDINAL
+{
+    i as ORDINAL
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect
new file mode 100644
index 0000000000..27442e7165
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-positive.dfy.expect
@@ -0,0 +1,4 @@
+conversion-positive.dfy(6,6): Error: a negative integer cannot be converted to an ORDINAL
+ Asserted expression: 0 <= i
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy
new file mode 100644
index 0000000000..f4669c1b8a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy
@@ -0,0 +1,9 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype uint8 = x: int | 0 <= x < 0x100
+
+function ConversionSatisfiesConstraints(i: int): uint8
+{
+    i as uint8
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect
new file mode 100644
index 0000000000..ae0bda188f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/conversion-satisfies-constraints.dfy.expect
@@ -0,0 +1,4 @@
+conversion-satisfies-constraints.dfy(8,6): Error: result of operation might violate newtype constraint for 'uint8'
+ Asserted expression: 0 <= i && i < 256
+
+Dafny program verifier finished with 1 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy
new file mode 100644
index 0000000000..4f66b4fc72
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method ForRangeAssignable()
+{
+    for i: nat := -1 to 0 {}
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect
new file mode 100644
index 0000000000..2d8b8ee4dd
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-assignable.dfy.expect
@@ -0,0 +1,4 @@
+for-range-assignable.dfy(6,8): Error: entire range must be assignable to index variable, but some value does not satisfy the subset constraints of 'nat'
+ Asserted expression: forall i: nat | -1 <= i && i <= 0 :: i is nat
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy
new file mode 100644
index 0000000000..a3e9447ffc
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method ForRangeBoundsValid()
+{
+    for _ := 1 to 0 {}
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect
new file mode 100644
index 0000000000..92376d7dd8
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/for-range-bounds-valid.dfy.expect
@@ -0,0 +1,4 @@
+for-range-bounds-valid.dfy(6,13): Error: lower bound must not exceed upper bound
+ Asserted expression: 1 <= 0
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy
new file mode 100644
index 0000000000..e463bb0f90
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method ForallPostcondition()
+{
+    forall b: bool ensures b {}
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect
new file mode 100644
index 0000000000..9d9598d6da
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/forall-postcondition.dfy.expect
@@ -0,0 +1,5 @@
+forall-postcondition.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
+forall-postcondition.dfy(6,27): Error: possible violation of postcondition of forall statement
+ Asserted expression: b
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy
new file mode 100644
index 0000000000..7828e20618
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy
@@ -0,0 +1,12 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C {
+    var f: int
+}
+
+method IsAllocated()
+{
+    var c := new C;
+    var f := old(c.f);
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect
new file mode 100644
index 0000000000..58098636c6
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-allocated.dfy.expect
@@ -0,0 +1,4 @@
+is-allocated.dfy(11,19): Error: receiver could not be proved to be allocated in the state in which its fields are accessed
+ Asserted expression: old(allocated(c))
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy
new file mode 100644
index 0000000000..037fca826f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function IsInteger(r: real): int
+{
+    r as int
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect
new file mode 100644
index 0000000000..f26b4291ba
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/is-integer.dfy.expect
@@ -0,0 +1,4 @@
+is-integer.dfy(6,6): Error: the real-based number must be an integer (if you want truncation, apply .Floor to the real-based number)
+ Asserted expression: r == r.Floor as real
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy
new file mode 100644
index 0000000000..4ebd45cdc9
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function NonNegative(): seq<int>
+{
+    seq(-1, i => 0)
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect
new file mode 100644
index 0000000000..c455e737cc
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-negative.dfy.expect
@@ -0,0 +1,4 @@
+non-negative.dfy(6,8): Error: sequence size might be negative
+ Asserted expression: 0 <= -1
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy
new file mode 100644
index 0000000000..60ddad634d
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy
@@ -0,0 +1,7 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function NonNull(a: array?<int>): int
+{
+    a.Length
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect
new file mode 100644
index 0000000000..44cf7fb11b
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/non-null.dfy.expect
@@ -0,0 +1,4 @@
+non-null.dfy(6,6): Error: target object might be null
+ Asserted expression: a != null
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy
new file mode 100644
index 0000000000..718073c345
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy
@@ -0,0 +1,8 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function OrdinalSubtractionIsNatural(o0: ORDINAL, o1: ORDINAL): ORDINAL
+    requires o1.Offset <= o0.Offset
+{
+    o0 - o1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect
new file mode 100644
index 0000000000..5fc5a9007a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-is-natural.dfy.expect
@@ -0,0 +1,4 @@
+ordinal-subtraction-is-natural.dfy(7,7): Error: RHS of ORDINAL subtraction must be a natural number, but the given RHS might be larger
+ Asserted expression: o1.IsNat
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy
new file mode 100644
index 0000000000..a852a5b313
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy
@@ -0,0 +1,8 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function OrdinalSubtractionUnderflow(o0: ORDINAL, o1: ORDINAL): ORDINAL
+    requires o1.IsNat
+{
+    o0 - o1
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect
new file mode 100644
index 0000000000..26480a9143
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/ordinal-subtraction-underflow.dfy.expect
@@ -0,0 +1,4 @@
+ordinal-subtraction-underflow.dfy(7,7): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
+ Asserted expression: o1.Offset <= o0.Offset
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy
new file mode 100644
index 0000000000..cb0e542d94
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function ShiftLowerBound(b: bv2): bv2 {
+    b.RotateLeft(-1)
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect
new file mode 100644
index 0000000000..6a6d539dc3
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-lower-bound.dfy.expect
@@ -0,0 +1,4 @@
+shift-lower-bound.dfy(5,6): Error: rotate amount must be non-negative
+ Asserted expression: 0 <= -1
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy
new file mode 100644
index 0000000000..35160e2c87
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy
@@ -0,0 +1,6 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function ShiftUpperBound(b: bv2): bv2 {
+    b.RotateLeft(3)
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect
new file mode 100644
index 0000000000..a0ead8362a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/shift-upper-bound.dfy.expect
@@ -0,0 +1,4 @@
+shift-upper-bound.dfy(5,6): Error: rotate amount must not exceed the width of the result (2)
+ Asserted expression: 3 <= 2
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy
new file mode 100644
index 0000000000..e713741a55
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy
@@ -0,0 +1,4 @@
+// RUN: %exits-with 4 %verify --show-proof-obligation-expressions "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype Pos = i: int | i > 0
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect
new file mode 100644
index 0000000000..cdf8c2ac7a
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/proof-obligation-desc/witness-check.dfy.expect
@@ -0,0 +1,4 @@
+witness-check.dfy(4,8): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+ Asserted expression: 0 > 0
+
+Dafny program verifier finished with 0 verified, 1 error