From a95131b9c35e33bc27972f06a554d1a6ac5bf904 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 19 May 2022 15:30:04 -0500
Subject: [PATCH] Initial pass, did all the proof obligation descriptions.

---
 .../Verifier/ProofObligationDescription.cs    | 556 ++++++++++++++++--
 .../Verifier/Translator.ClassMembers.cs       |  18 +-
 .../Verifier/Translator.TrStatement.cs        |   4 +-
 Source/DafnyCore/Verifier/Translator.cs       | 148 +++--
 Source/DafnyPipeline.Test/TranslatorTest.cs   | 301 ++++++++++
 5 files changed, 916 insertions(+), 111 deletions(-)

diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs
index 94e527a1faf..e27c07752fe 100644
--- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs
+++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs
@@ -1,10 +1,59 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Reflection.Emit;
 using JetBrains.Annotations;
+using Microsoft.BaseTypes;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny.ProofObligationDescription;
 
 public abstract class ProofObligationDescription : Boogie.ProofObligationDescription {
+  public abstract Expression GetAssertedExpr(DafnyOptions options);
+}
+
+// When there is no way to translate the asserted constraint in Dafny
+public abstract class ProofObligationDescriptionNotInDafny : ProofObligationDescription {
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return null;
+  }
+}
+
+// when the constraint is already computed in the translator, so no need to compute it.
+public abstract class ProofObligationDescriptionWithExplicitConstraint : ProofObligationDescription {
+  private readonly Expression constraint;
+
+  protected ProofObligationDescriptionWithExplicitConstraint(Expression constraint) {
+    this.constraint = constraint;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return constraint;
+  }
+}
+
+// When one proof obligation description asserts on multiple expressions at the same time
+public abstract class AndProofObligationDescription : ProofObligationDescription {
+  private Expression[] whatExprs;
+
+  protected AndProofObligationDescription(Expression[] whatExprs) {
+    this.whatExprs = whatExprs;
+  }
+
+  public abstract Expression GetSingleAssertExpr(Expression whatExpr);
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    var resultExpression = whatExprs.Length == 0 ? (Expression)new LiteralExpr(Token.NoToken, true) :
+      GetSingleAssertExpr(whatExprs[0]);
+
+    for (var i = 1; i < whatExprs.Length; i++) {
+      resultExpression = new BinaryExpr(whatExprs[i].tok, BinaryExpr.Opcode.And,
+        resultExpression,
+        GetSingleAssertExpr(whatExprs[i])
+      );
+    }
+    return resultExpression;
+  }
 }
 
 //// Arithmetic and logical operators, conversions
@@ -17,6 +66,16 @@ public class DivisorNonZero : ProofObligationDescription {
     "possible division by zero";
 
   public override string ShortDescription => "non-zero divisor";
+
+  private readonly Expression divisor;
+
+  public DivisorNonZero(Expression divisor) {
+    this.divisor = divisor;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(divisor.tok, BinaryExpr.Opcode.Neq, divisor, new LiteralExpr(divisor.tok, 0));
+  }
 }
 
 public class ShiftLowerBound : ProofObligationDescription {
@@ -27,6 +86,16 @@ public class ShiftLowerBound : ProofObligationDescription {
     "shift amount must be non-negative";
 
   public override string ShortDescription => "shift lower bound";
+
+  private readonly Expression shiftAmount;
+
+  public ShiftLowerBound(Expression shiftAmount) {
+    this.shiftAmount = shiftAmount;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(shiftAmount.tok, BinaryExpr.Opcode.Ge, shiftAmount, new LiteralExpr(shiftAmount.tok, 0));
+  }
 }
 
 public class ShiftUpperBound : ProofObligationDescription {
@@ -38,14 +107,20 @@ public class ShiftUpperBound : ProofObligationDescription {
 
   public override string ShortDescription => "shift upper bound";
 
+  private readonly Expression shiftAmount;
   private readonly int width;
 
-  public ShiftUpperBound(int width) {
+  public ShiftUpperBound(Expression shiftAmount, int width) {
+    this.shiftAmount = shiftAmount;
     this.width = width;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(shiftAmount.tok, BinaryExpr.Opcode.Le, shiftAmount, new LiteralExpr(shiftAmount.tok, width));
+  }
 }
 
-public class ConversionIsNatural : ProofObligationDescription {
+public class ConversionIsNatural : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"{prefix}value to be converted is always a natural number";
 
@@ -61,7 +136,7 @@ public class ConversionIsNatural : ProofObligationDescription {
   }
 }
 
-public class ConversionSatisfiesConstraints : ProofObligationDescription {
+public class ConversionSatisfiesConstraints : ProofObligationDescriptionWithExplicitConstraint {
   public override string SuccessDescription =>
     $"{prefix}result of operation never violates {kind} constraints for '{name}'";
 
@@ -74,14 +149,15 @@ public class ConversionSatisfiesConstraints : ProofObligationDescription {
   private readonly string kind;
   private readonly string name;
 
-  public ConversionSatisfiesConstraints(string prefix, string kind, string name) {
+  public ConversionSatisfiesConstraints(string prefix, string kind, string name, Expression constraint) :
+      base(constraint) {
     this.prefix = prefix;
     this.kind = kind;
     this.name = name;
   }
 }
 
-public class OrdinalSubtractionIsNatural : ProofObligationDescription {
+public class OrdinalSubtractionIsNatural : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     "RHS of ORDINAL subtraction is always a natural number";
 
@@ -91,7 +167,7 @@ public class OrdinalSubtractionIsNatural : ProofObligationDescription {
   public override string ShortDescription => "ordinal subtraction is natural";
 }
 
-public class OrdinalSubtractionUnderflow : ProofObligationDescription {
+public class OrdinalSubtractionUnderflow : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     "ORDINAL subtraction will never go below limit ordinal";
 
@@ -102,6 +178,9 @@ public class OrdinalSubtractionUnderflow : ProofObligationDescription {
 }
 
 public class CharOverflow : ProofObligationDescription {
+  private readonly Expression e0;
+  private readonly Expression e1;
+
   public override string SuccessDescription =>
     "char addition will not overflow";
 
@@ -109,9 +188,24 @@ public class CharOverflow : ProofObligationDescription {
     "char addition might overflow";
 
   public override string ShortDescription => "char overflow";
+
+  public CharOverflow(Expression e0, Expression e1) {
+    this.e0 = e0;
+    this.e1 = e1;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le,
+      new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add,
+        new ConversionExpr(e0.tok, e0, Type.Int),
+        new ConversionExpr(e1.tok, e1, Type.Int)
+      ), new LiteralExpr(e0.tok, 65536));
+  }
 }
 
 public class CharUnderflow : ProofObligationDescription {
+  private readonly Expression e0;
+  private readonly Expression e1;
+
   public override string SuccessDescription =>
     "char subtraction will not underflow";
 
@@ -119,6 +213,18 @@ public class CharUnderflow : ProofObligationDescription {
     "char subtraction might underflow";
 
   public override string ShortDescription => "char underflow";
+
+  public CharUnderflow(Expression e0, Expression e1) {
+    this.e0 = e0;
+    this.e1 = e1;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(e0.tok, BinaryExpr.Opcode.Ge,
+      new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add,
+        new ConversionExpr(e0.tok, e0, Type.Int),
+        new ConversionExpr(e1.tok, e1, Type.Int)
+      ), new LiteralExpr(e0.tok, 0));
+  }
 }
 
 public class ConversionFit : ProofObligationDescription {
@@ -133,11 +239,50 @@ public class ConversionFit : ProofObligationDescription {
   private readonly string prefix;
   private readonly string what;
   private readonly Type toType;
+  private readonly Expression expr;
+  private readonly BigInteger width;
 
-  public ConversionFit(string what, Type toType, string prefix = "") {
+  public ConversionFit(string what, Type toType, Expression expr, BigInteger width, string prefix = "") {
     this.prefix = prefix;
     this.what = what;
     this.toType = toType;
+    this.expr = expr;
+    this.width = width;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    if (width.IsZero) {
+      if (toType.IsCharType) {
+        Expression ToBound(int value) {
+          return expr.Type.IsNumericBased(Type.NumericPersuasion.Real) ? new LiteralExpr(expr.tok, BigDec.FromInt(value)) : new LiteralExpr(expr.tok, value);
+        }
+        if (options.UnicodeOutput) {
+          return
+            new BinaryExpr(expr.Tok, BinaryExpr.Opcode.Or,
+              new BinaryExpr(expr.Tok, BinaryExpr.Opcode.And,
+                new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, ToBound(0),
+                  expr),
+                new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, ToBound(0xD800))
+              ),
+              new BinaryExpr(expr.Tok, BinaryExpr.Opcode.And,
+                new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, ToBound(0xE000),
+                  expr),
+                new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, ToBound(0x11_0000))
+              ));
+        }
+        return new BinaryExpr(expr.Tok, BinaryExpr.Opcode.And,
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, ToBound(0),
+            expr),
+          new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr, ToBound(65536))
+        );
+      }
+
+      return null; // Not yet supported
+    }
+    return new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, expr,
+      new BinaryExpr(expr.tok, BinaryExpr.Opcode.LeftShift,
+        new LiteralExpr(expr.tok, 1), new LiteralExpr(expr.tok, width))
+    );
   }
 }
 
@@ -151,9 +296,15 @@ public class NonNegative : ProofObligationDescription {
   public override string ShortDescription => "non-negative";
 
   private readonly string what;
+  private readonly Expression whatExpr;
 
-  public NonNegative(string what) {
+  public NonNegative(string what, Expression whatExpr) {
     this.what = what;
+    this.whatExpr = whatExpr;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(whatExpr.tok, BinaryExpr.Opcode.Gt, whatExpr, new LiteralExpr(whatExpr.tok, 0));
   }
 }
 
@@ -169,11 +320,20 @@ 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) {
+    Expression ToBound(int value) {
+      return expr.Type.IsNumericBased(Type.NumericPersuasion.Real) ? new LiteralExpr(expr.tok, BigDec.FromInt(value)) : new LiteralExpr(expr.tok, value);
+    }
+
+    return new BinaryExpr(expr.tok, BinaryExpr.Opcode.Lt, ToBound(0), expr);
   }
 }
 
@@ -186,16 +346,26 @@ public class IsInteger : ProofObligationDescription {
 
   public override string ShortDescription => "is integer";
 
+  private readonly Expression whatExpr;
   private readonly string prefix;
 
-  public IsInteger(string prefix = "") {
+  public IsInteger(Expression whatExpr, string prefix = "") {
+    this.whatExpr = whatExpr;
     this.prefix = prefix;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return
+      new BinaryExpr(whatExpr.Tok, BinaryExpr.Opcode.Eq,
+        new ConversionExpr(whatExpr.Tok,
+          new MemberSelectExpr(whatExpr.Tok, whatExpr, "Floor"),
+          Type.Real), whatExpr);
+  }
 }
 
 //// Object properties
 
-public class NonNull : ProofObligationDescription {
+public class NonNull : AndProofObligationDescription {
   public override string SuccessDescription =>
     $"{PluralSuccess}{what} object is never null";
 
@@ -203,18 +373,23 @@ public class NonNull : ProofObligationDescription {
     $"{PluralFailure}{what} might be null";
 
   public override string ShortDescription => $"{what} non-null";
+
   private readonly string what;
   private bool plural;
   private string PluralSuccess => plural ? "each " : "";
   private string PluralFailure => plural ? "some " : "";
 
-  public NonNull(string what, bool plural = false) {
+  public NonNull(Expression[] whatExprs, string what, bool plural = false) : base(whatExprs) {
     this.what = what;
     this.plural = plural;
   }
+
+  public override Expression GetSingleAssertExpr(Expression whatExpr) {
+    return new BinaryExpr(whatExpr.tok, BinaryExpr.Opcode.Neq, whatExpr, new LiteralExpr(whatExpr.tok));
+  }
 }
 
-public class IsAllocated : ProofObligationDescription {
+public class IsAllocated : AndProofObligationDescription {
   public override string SuccessDescription =>
     $"{PluralSuccess}{what} is always allocated{WhenSuffix}";
 
@@ -230,14 +405,18 @@ public class IsAllocated : ProofObligationDescription {
   private string PluralSuccess => plural ? "each " : "";
   private string PluralFailure => plural ? "some " : "";
 
-  public IsAllocated(string what, string when, bool plural = false) {
+  public IsAllocated(Expression[] whatExprs, string what, string when, bool plural = false) : base(whatExprs) {
     this.what = what;
     this.when = when;
     this.plural = plural;
   }
+
+  public override Expression GetSingleAssertExpr(Expression whatExpr) {
+    return new UnaryOpExpr(whatExpr.tok, UnaryOpExpr.Opcode.Allocated, whatExpr);
+  }
 }
 
-public class IsOlderProofObligation : ProofObligationDescription {
+public class IsOlderProofObligation : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription {
     get {
       var successOlder = olderParameterCount == 1 ? " is" : "s are";
@@ -272,7 +451,7 @@ public class IsOlderProofObligation : ProofObligationDescription {
 
 //// Contract constraints
 
-public class PreconditionSatisfied : ProofObligationDescription {
+public class PreconditionSatisfied : ProofObligationDescriptionWithExplicitConstraint {
   public override string SuccessDescription =>
     customErrMsg is null
       ? "function precondition satisfied"
@@ -283,14 +462,19 @@ public class PreconditionSatisfied : ProofObligationDescription {
 
   public override string ShortDescription => "precondition";
 
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    throw new System.NotImplementedException();
+  }
+
   private readonly string customErrMsg;
 
-  public PreconditionSatisfied([CanBeNull] string customErrMsg) {
+  public PreconditionSatisfied([CanBeNull] string customErrMsg, Expression constraint) : base(constraint) {
     this.customErrMsg = customErrMsg;
   }
 }
 
-public class AssertStatement : ProofObligationDescription {
+public class AssertStatement : ProofObligationDescriptionWithExplicitConstraint {
+  public bool Splitted { get; set; }
   public override string SuccessDescription =>
     customErrMsg is null
       ? "assertion always holds"
@@ -303,12 +487,13 @@ public class AssertStatement : ProofObligationDescription {
 
   private readonly string customErrMsg;
 
-  public AssertStatement([CanBeNull] string customErrMsg) {
+  public AssertStatement([CanBeNull] string customErrMsg, Expression constraint, bool splitted = false) : base(constraint) {
+    this.Splitted = splitted;
     this.customErrMsg = customErrMsg;
   }
 }
 
-public class LoopInvariant : ProofObligationDescription {
+public class LoopInvariant : ProofObligationDescriptionWithExplicitConstraint {
   public override string SuccessDescription =>
     customErrMsg is null
       ? "loop invariant always holds"
@@ -321,12 +506,16 @@ public class LoopInvariant : ProofObligationDescription {
 
   private readonly string customErrMsg;
 
-  public LoopInvariant([CanBeNull] string customErrMsg) {
+  public LoopInvariant([CanBeNull] string customErrMsg, Expression constraint) : base(constraint) {
     this.customErrMsg = customErrMsg;
   }
 }
 
 public class CalculationStep : ProofObligationDescription {
+  private readonly Expression before;
+  private readonly Expression after;
+  private readonly BinaryExpr.Opcode operandType;
+
   public override string SuccessDescription =>
     "the calculation step between the previous line and this line always holds";
 
@@ -334,6 +523,16 @@ public class CalculationStep : ProofObligationDescription {
     "the calculation step between the previous line and this line might not hold";
 
   public override string ShortDescription => "calc step";
+
+  public CalculationStep(Expression before, Expression after, BinaryExpr.Opcode operandType) {
+    this.before = before;
+    this.after = after;
+    this.operandType = operandType;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(before.tok, operandType, before, after);
+  }
 }
 
 public class EnsuresStronger : ProofObligationDescription {
@@ -344,6 +543,10 @@ public class EnsuresStronger : ProofObligationDescription {
     "the method must provide an equal or more detailed postcondition than in its parent trait";
 
   public override string ShortDescription => "ensures stronger";
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    // TODO
+    return null;
+  }
 }
 
 public class RequiresWeaker : ProofObligationDescription {
@@ -354,9 +557,14 @@ public class RequiresWeaker : ProofObligationDescription {
     "the method must provide an equal or more permissive precondition than in its parent trait";
 
   public override string ShortDescription => "requires weaker";
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    // TODO
+    return null;
+  }
 }
 
-public class ForallPostcondition : ProofObligationDescription {
+public class ForallPostcondition : ProofObligationDescriptionWithExplicitConstraint {
   public override string SuccessDescription =>
     "postcondition of forall statement always holds";
 
@@ -364,6 +572,9 @@ public class ForallPostcondition : ProofObligationDescription {
     "possible violation of postcondition of forall statement";
 
   public override string ShortDescription => "forall ensures";
+
+  public ForallPostcondition(Expression constraint) : base(constraint) {
+  }
 }
 
 public class YieldEnsures : ProofObligationDescription {
@@ -374,6 +585,10 @@ public class YieldEnsures : ProofObligationDescription {
     "possible violation of yield-ensures condition";
 
   public override string ShortDescription => "yield ensures";
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 public class TraitFrame : ProofObligationDescription {
@@ -397,6 +612,10 @@ public class TraitFrame : ProofObligationDescription {
     this.whatKind = whatKind;
     this.isModify = isModify;
   }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 public class TraitDecreases : ProofObligationDescription {
@@ -413,6 +632,11 @@ public class TraitDecreases : ProofObligationDescription {
   public TraitDecreases(string whatKind) {
     this.whatKind = whatKind;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 public class FrameSubset : ProofObligationDescription {
@@ -435,6 +659,11 @@ public class FrameSubset : ProofObligationDescription {
     this.whatKind = whatKind;
     this.isWrite = isWrite;
   }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 public class FrameDereferenceNonNull : ProofObligationDescription {
@@ -445,6 +674,11 @@ public class FrameDereferenceNonNull : ProofObligationDescription {
     "frame expression might dereference null";
 
   public override string ShortDescription => "frame dereference";
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 public class Terminates : ProofObligationDescription {
@@ -458,16 +692,75 @@ public class Terminates : ProofObligationDescription {
     (hint is null ? "" : $" ({hint})");
 
   public override string ShortDescription => "termination";
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    // Given [A0, A1, A2, A3] and [B0, B1, B2, B3]
+    // - For Boogie, we compute a quadratic encoding
+    // && (A0 < B0 || A0 == B0)
+    // && (A0 < B0 || A1 < B1 || A1 == B1)
+    // && (A0 < B0 || A1 < B1 || A2 < B2 || A2 == B2)
+    // && (A0 < B0 || A1 < B1 || A2 < B2 || A3 < B3 || A3 == B3)
+    // - For Dafny users, we use the linear encoding
+    // A0 < B0 || (A0 == B0 && (A1 < B1 || (A1 == B1 && (A2 < B2 || (A2 == B2 && A3 < B3))))
+
+    Expression constraint = null;
+    for (var i = calleeDecreasesFinal.Count - 1; i >= 0; i++) {
+      Expression lessThan;
+      var A = calleeDecreasesFinal[i];
+      var B = contextDecreasesFinal[i];
+      if (A.Type.IsNumericBased(Type.NumericPersuasion.Int) ||
+          A.Type.IsNumericBased(Type.NumericPersuasion.Real) ||
+          A.Type is CharType ||
+          A.Type.AsDatatype != null) {
+        lessThan = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Lt, A, B);
+      } else if (A.Type.IsBoolType) {
+        lessThan = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And, new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Not, A), B);
+      } else if (A.Type.AsSeqType != null) {
+        lessThan = new BinaryExpr(
+          Token.NoToken, BinaryExpr.Opcode.And,
+          new BinaryExpr(
+            Token.NoToken, BinaryExpr.Opcode.Lt,
+            new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, A),
+            new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, B)),
+          new BinaryExpr(
+            Token.NoToken, BinaryExpr.Opcode.Eq,
+            A,
+            new SeqSelectExpr(Token.NoToken, false, B,
+              new LiteralExpr(Token.NoToken, 0),
+              new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Cardinality, A), Token.NoToken)));
+      } else {
+        return null; // Don't know how to handle that
+      }
+
+      if (constraint == null) {
+        constraint = lessThan;
+      } else {
+        constraint = new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Or,
+          lessThan,
+          new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.And,
+            new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Eq,
+              A, B
+            ),
+            constraint
+          ));
+      }
+    }
+
+    return constraint;
+  }
 
   private readonly bool inferredDescreases;
   private readonly bool isLoop;
   private readonly string hint;
+  private readonly List<Expression> contextDecreasesFinal;
+  private readonly List<Expression> calleeDecreasesFinal;
   private string FormDescription => isLoop ? "expression" : "clause";
 
-  public Terminates(bool inferredDescreases, bool isLoop, string hint = null) {
+  public Terminates(List<Expression> contextDecreasesFinal, List<Expression> calleeDecreasesFinal, bool inferredDescreases, bool isLoop, string hint = null) {
     this.inferredDescreases = inferredDescreases;
     this.isLoop = isLoop;
     this.hint = hint;
+    this.contextDecreasesFinal = contextDecreasesFinal;
+    this.calleeDecreasesFinal = calleeDecreasesFinal;
   }
 }
 
@@ -483,17 +776,24 @@ public class DecreasesBoundedBelow : ProofObligationDescription {
   private string component => N == 1 ? "expression" : $"expression at index {k}";
   private readonly string zeroStr;
   private readonly string suffix;
+  private readonly Expression expression;
+  private readonly Expression zeroExpr;
   private readonly int N, k;
 
-  public DecreasesBoundedBelow(int N, int k, string zeroStr, string suffix) {
+  public DecreasesBoundedBelow(int N, int k, string zeroStr, string suffix, Expression expression, Expression zeroExpr) {
     this.N = N;
     this.k = k;
     this.zeroStr = zeroStr;
     this.suffix = suffix;
+    this.expression = expression;
+    this.zeroExpr = zeroExpr;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(expression.tok, BinaryExpr.Opcode.Ge, expression, zeroExpr);
   }
 }
 
-public class Modifiable : ProofObligationDescription {
+public class Modifiable : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"{description} is in the enclosing context's modifies clause";
 
@@ -525,11 +825,15 @@ public class FunctionContractOverride : ProofObligationDescription {
   public FunctionContractOverride(bool isEnsures) {
     this.isEnsures = isEnsures;
   }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    //TODO
+    return null;
+  }
 }
 
 //// Structural constraints
 
-public class MatchIsComplete : ProofObligationDescription {
+public class MatchIsComplete : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"match {matchForm} covers all cases";
 
@@ -546,7 +850,7 @@ public class MatchIsComplete : ProofObligationDescription {
   }
 }
 
-public class AlternativeIsComplete : ProofObligationDescription {
+public class AlternativeIsComplete : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"alternative cases cover all possibilties";
 
@@ -556,7 +860,7 @@ public class AlternativeIsComplete : ProofObligationDescription {
   public override string ShortDescription => "alternative complete";
 }
 
-public class PatternShapeIsValid : ProofObligationDescription {
+public class PatternShapeIsValid : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"RHS will always match the pattern '{ctorName}'";
 
@@ -572,7 +876,7 @@ public class PatternShapeIsValid : ProofObligationDescription {
   }
 }
 
-public class ValidConstructorNames : ProofObligationDescription {
+public class ValidConstructorNames : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"source of datatype update is constructed by {ctorNames}";
 
@@ -588,7 +892,7 @@ public class ValidConstructorNames : ProofObligationDescription {
   }
 }
 
-public class DestructorValid : ProofObligationDescription {
+public class DestructorValid : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"destructor '{dtorName}' is only applied to datatype values constructed by {ctorNames}";
 
@@ -606,7 +910,7 @@ public class DestructorValid : ProofObligationDescription {
   }
 }
 
-public class NotGhostVariant : ProofObligationDescription {
+public class NotGhostVariant : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"in a compiled context, {subject} is not applied to a datatype value of a ghost variant (ghost constructor {ctorNames})";
 
@@ -632,7 +936,7 @@ public class NotGhostVariant : ProofObligationDescription {
 
 //// Misc constraints
 
-public class IndicesInDomain : ProofObligationDescription {
+public class IndicesInDomain : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"all {objType} indices are in the domain of the initialization function";
 
@@ -648,7 +952,7 @@ public class IndicesInDomain : ProofObligationDescription {
   }
 }
 
-public class SubrangeCheck : ProofObligationDescription {
+public class SubrangeCheck : ProofObligationDescriptionWithExplicitConstraint {
   public override string SuccessDescription =>
     isSubset
       ? $"value always satisfies the subset constraints of '{targetType}'"
@@ -671,7 +975,7 @@ public class SubrangeCheck : ProofObligationDescription {
   private readonly bool isCertain;
   private readonly string cause;
 
-  public SubrangeCheck(string prefix, string sourceType, string targetType, bool isSubset, bool isCertain, [CanBeNull] string cause) {
+  public SubrangeCheck(string prefix, string sourceType, string targetType, bool isSubset, bool isCertain, [CanBeNull] string cause, Expression constraint) : base(constraint) {
     this.prefix = prefix;
     this.sourceType = sourceType;
     this.targetType = targetType;
@@ -696,13 +1000,28 @@ public class WitnessCheck : ProofObligationDescription {
   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;
+  private readonly RedirectingTypeDecl typeDecl;
+  private readonly Expression witnessExpr;
 
-  public WitnessCheck(string witnessString) {
+  public WitnessCheck(string witnessString, RedirectingTypeDecl typeDecl, Expression witnessExpr) {
     this.witnessString = witnessString;
+    this.typeDecl = typeDecl;
+    this.witnessExpr = witnessExpr;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    if (witnessExpr == null) {
+      return null;
+    }
+    return new LetExpr(witnessExpr.tok, new List<CasePattern<BoundVar>>() {
+        new(witnessExpr.tok, typeDecl.Var)
+      }, new List<Expression>() { witnessExpr },
+      typeDecl.Constraint, true);
   }
 }
 
 public class PrefixEqualityLimit : ProofObligationDescription {
+  private readonly Expression exprAtLeastZero;
+
   public override string SuccessDescription =>
     "prefix-equality limit is at least 0";
 
@@ -710,9 +1029,19 @@ public class PrefixEqualityLimit : ProofObligationDescription {
     "prefix-equality limit must be at least 0";
 
   public override string ShortDescription => "prefix-equality limit";
+  public PrefixEqualityLimit(Expression exprAtLeastZero) {
+    this.exprAtLeastZero = exprAtLeastZero;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(exprAtLeastZero.tok, BinaryExpr.Opcode.Le,
+      new LiteralExpr(exprAtLeastZero.tok, 0), exprAtLeastZero);
+  }
 }
 
 public class ForRangeBoundsValid : ProofObligationDescription {
+  private readonly Expression lowerExpr;
+  private readonly Expression upperExpr;
+
   public override string SuccessDescription =>
     "lower bound does not exceed upper bound";
 
@@ -720,6 +1049,14 @@ public class ForRangeBoundsValid : ProofObligationDescription {
     "lower bound must not exceed upper bound";
 
   public override string ShortDescription => "for range bounds";
+  public ForRangeBoundsValid(Expression lowerExpr, Expression upperExpr) {
+    this.lowerExpr = lowerExpr;
+    this.upperExpr = upperExpr;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(lowerExpr.tok, BinaryExpr.Opcode.Le,
+      lowerExpr, upperExpr);
+  }
 }
 
 public class ForRangeAssignable : ProofObligationDescription {
@@ -732,13 +1069,32 @@ public class ForRangeAssignable : ProofObligationDescription {
   public override string ShortDescription => "for range assignable";
 
   private readonly ProofObligationDescription desc;
+  private readonly BoundVar variable;
+  private readonly int low;
+  private readonly int high;
+  private readonly Type expectedType;
 
-  public ForRangeAssignable(ProofObligationDescription desc) {
+  public ForRangeAssignable(ProofObligationDescription desc, BoundVar variable, int low, int high, Type expectedType) {
     this.desc = desc;
+    this.variable = variable;
+    this.low = low;
+    this.high = high;
+    this.expectedType = expectedType;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    var variableExpr = new IdentifierExpr(variable.tok, variable);
+    return new ForallExpr(variable.tok, variable.RangeToken, new List<BoundVar>() { variable },
+      new BinaryExpr(variable.tok, BinaryExpr.Opcode.And,
+        new BinaryExpr(variable.tok, BinaryExpr.Opcode.Le, new LiteralExpr(variable.tok, low),
+          variableExpr),
+        new BinaryExpr(variable.tok, BinaryExpr.Opcode.Le, variableExpr,
+          new LiteralExpr(variable.tok, high))
+      ), new TypeTestExpr(variable.tok, variableExpr, expectedType), null);
   }
 }
 
-public class ValidInRecursion : ProofObligationDescription {
+public class ValidInRecursion : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"{what} is valid in recursive setting";
 
@@ -756,7 +1112,7 @@ public class ValidInRecursion : ProofObligationDescription {
   }
 }
 
-public class IsNonRecursive : ProofObligationDescription {
+public class IsNonRecursive : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     "default value is non-recursive";
 
@@ -766,7 +1122,7 @@ public class IsNonRecursive : ProofObligationDescription {
   public override string ShortDescription => "default nonrecursive";
 }
 
-public class ForallLHSUnique : ProofObligationDescription {
+public class ForallLHSUnique : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     "left-hand sides of forall-statement bound variables are unique";
 
@@ -777,6 +1133,9 @@ public class ForallLHSUnique : ProofObligationDescription {
 }
 
 public class ElementInDomain : ProofObligationDescription {
+  private readonly Expression sequence;
+  private readonly Expression index;
+
   public override string SuccessDescription =>
     "element is in domain";
 
@@ -784,9 +1143,21 @@ public class ElementInDomain : ProofObligationDescription {
     "element might not be in domain";
 
   public override string ShortDescription => "element in domain";
+
+
+  public ElementInDomain(Expression sequence, Expression index) {
+    this.sequence = sequence;
+    this.index = index;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(sequence.tok, BinaryExpr.Opcode.In,
+      index,
+      sequence
+    );
+  }
 }
 
-public class DefiniteAssignment : ProofObligationDescription {
+public class DefiniteAssignment : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"{what}, which is subject to definite-assignment rules, is always initialized {where}";
 
@@ -805,17 +1176,34 @@ public class DefiniteAssignment : ProofObligationDescription {
 }
 
 public class InRange : ProofObligationDescription {
+  private readonly Expression sequence;
+  private readonly Expression index;
+  private readonly string what;
   public override string SuccessDescription => $"{what} in range";
 
   public override string FailureDescription => $"{what} out of range";
 
   public override string ShortDescription => "in range";
 
-  private readonly string what;
-
-  public InRange(string what) {
+  public InRange(Expression sequence, Expression index, string what) {
+    this.sequence = sequence;
+    this.index = index;
     this.what = what;
   }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    if (sequence.Type is SeqType) {
+      return new BinaryExpr(sequence.tok, BinaryExpr.Opcode.And,
+        new BinaryExpr(sequence.tok, BinaryExpr.Opcode.Le, new LiteralExpr(sequence.tok, 0), index),
+        new BinaryExpr(sequence.tok, BinaryExpr.Opcode.Le, index,
+          new UnaryOpExpr(sequence.tok, UnaryOpExpr.Opcode.Cardinality, sequence))
+      );
+    }
+
+    return new BinaryExpr(sequence.tok, BinaryExpr.Opcode.In,
+      index,
+      sequence
+    );
+  }
 }
 
 public class SequenceSelectRangeValid : ProofObligationDescription {
@@ -828,13 +1216,32 @@ public class SequenceSelectRangeValid : ProofObligationDescription {
   public override string ShortDescription => "sequence select range valid";
 
   private readonly string what;
+  private readonly Expression sequence;
+  private readonly Expression lowerBound;
+  private readonly Expression upperBound;
 
-  public SequenceSelectRangeValid(string what) {
+  public SequenceSelectRangeValid(string what, Expression sequence, Expression lowerBound, Expression upperBound) {
     this.what = what;
+    this.sequence = sequence;
+    this.lowerBound = lowerBound;
+    this.upperBound = upperBound;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(sequence.tok, BinaryExpr.Opcode.And,
+      new BinaryExpr(sequence.tok, BinaryExpr.Opcode.Le, lowerBound, upperBound),
+      new BinaryExpr(sequence.tok, BinaryExpr.Opcode.Le, upperBound,
+        new UnaryOpExpr(sequence.tok, UnaryOpExpr.Opcode.Cardinality, sequence))
+      );
   }
 }
 
 public class ComprehensionNoAlias : ProofObligationDescription {
+  private readonly Expression bodyLeft;
+  private readonly Expression bodyLeftPrime;
+  private readonly Expression body;
+  private readonly Expression bodyPrime;
+
   public override string SuccessDescription =>
     "key expressions refer to unique values";
 
@@ -842,9 +1249,22 @@ public class ComprehensionNoAlias : ProofObligationDescription {
     "key expressions might be referring to the same value";
 
   public override string ShortDescription => "unique key expressions";
+
+  public ComprehensionNoAlias(Expression bodyLeft, Expression bodyLeftPrime, Expression body, Expression bodyPrime) {
+    this.bodyLeft = bodyLeft;
+    this.bodyLeftPrime = bodyLeftPrime;
+    this.body = body;
+    this.bodyPrime = bodyPrime;
+  }
+
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new BinaryExpr(body.tok, BinaryExpr.Opcode.Or,
+      new BinaryExpr(body.tok, BinaryExpr.Opcode.Neq, bodyLeft, bodyLeftPrime),
+      new BinaryExpr(body.tok, BinaryExpr.Opcode.Eq, body, bodyPrime));
+  }
 }
 
-public class DistinctLHS : ProofObligationDescription {
+public class DistinctLHS : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"left-hand sides {lhsa} and {lhsb} are distinct";
 
@@ -868,7 +1288,7 @@ public class DistinctLHS : ProofObligationDescription {
   }
 }
 
-public class ArrayInitSizeValid : ProofObligationDescription {
+public class ArrayInitSizeValid : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"given array size agrees with the number of expressions in the initializing display ({size})";
 
@@ -884,7 +1304,7 @@ public class ArrayInitSizeValid : ProofObligationDescription {
   }
 }
 
-public class ArrayInitEmpty : ProofObligationDescription {
+public class ArrayInitEmpty : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     "array initializer has empty size";
 
@@ -901,6 +1321,9 @@ public class ArrayInitEmpty : ProofObligationDescription {
 }
 
 public class LetSuchThanUnique : ProofObligationDescription {
+  private readonly Expression condition;
+  private readonly BoundVar boundVar;
+
   public override string SuccessDescription =>
     "the value of this let-such-that expression is uniquely determined";
 
@@ -908,9 +1331,33 @@ public class LetSuchThanUnique : ProofObligationDescription {
     "to be compilable, the value of a let-such-that expression must be uniquely determined";
 
   public override string ShortDescription => "let-such-that unique";
+
+  public LetSuchThanUnique(Expression condition, BoundVar boundVar) {
+    this.condition = condition;
+    this.boundVar = boundVar;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    Expression boundVarExpr = new IdentifierExpr(boundVar.tok, boundVar);
+    BoundVar secondBoundVar = new BoundVar(boundVar.tok, boundVar.Name + "'", boundVar.Type);
+    Expression secondBoundVarExpr = new IdentifierExpr(secondBoundVar.tok, secondBoundVar);
+    var subContract = new Substituter(null,
+      new Dictionary<IVariable, Expression>()
+      {
+        {boundVar, secondBoundVarExpr}
+      },
+      new Dictionary<TypeParameter, Type>()
+    );
+    var conditionSecondBoundVar = subContract.Substitute(condition);
+    return new ForallExpr(boundVar.tok, boundVar.RangeToken, new List<BoundVar>() { boundVar, secondBoundVar },
+      new BinaryExpr(boundVar.tok, BinaryExpr.Opcode.And, condition, conditionSecondBoundVar),
+      new BinaryExpr(boundVar.tok, BinaryExpr.Opcode.Eq, boundVarExpr, secondBoundVarExpr), null);
+  }
 }
 
-public class LetSuchThanExists : ProofObligationDescription {
+public class LetSuchThatExists : ProofObligationDescription {
+  private readonly Expression condition;
+  private readonly List<BoundVar> bvars;
+
   public override string SuccessDescription =>
     "a value exists that satisfies this let-such-that expression";
 
@@ -918,9 +1365,18 @@ public class LetSuchThanExists : ProofObligationDescription {
     "cannot establish the existence of LHS values that satisfy the such-that predicate";
 
   public override string ShortDescription => "let-such-that exists";
+
+  public LetSuchThatExists(List<BoundVar> bvars, Expression condition) {
+    this.condition = condition;
+    this.bvars = bvars;
+  }
+  public override Expression GetAssertedExpr(DafnyOptions options) {
+    return new ExistsExpr(bvars[0].tok, bvars[0].RangeToken, bvars,
+      condition, new LiteralExpr(bvars[0].tok, true), null);
+  }
 }
 
-public class AssignmentShrinks : ProofObligationDescription {
+public class AssignmentShrinks : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"the assignment to {fieldName} always shrinks the set";
 
@@ -936,7 +1392,7 @@ public class AssignmentShrinks : ProofObligationDescription {
   }
 }
 
-public class BoilerplateTriple : ProofObligationDescription {
+public class BoilerplateTriple : ProofObligationDescriptionNotInDafny {
   public override string SuccessDescription =>
     $"error is impossible: {msg}";
 
diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
index 60cb83a5b33..d59944d5734 100644
--- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
+++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs
@@ -669,7 +669,7 @@ public partial class Translator {
           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(new Expression[] { e }, "default value", "in the two-state lemma's previous state");
               builder.Add(Assert(e.tok, wh, desc));
             }
           }
@@ -1412,7 +1412,7 @@ public partial class Translator {
           if (formal.IsOld) {
             var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal);
             var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
-            var desc = new PODesc.IsAllocated($"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state");
+            var desc = new PODesc.IsAllocated(new Expression[] { dafnyFormalIdExpr }, $"parameter{pIdx} ('{formal.Name}')", "in the two-state lemma's previous state");
             var require = Requires(formal.tok, false, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
               desc.FailureDescription, null);
             require.Description = desc;
@@ -1451,7 +1451,7 @@ public partial class Translator {
         comment = "user-defined postconditions";
         foreach (var p in m.Ens) {
           string errorMessage = CustomErrorMessage(p.Attributes);
-          AddEnsures(ens, Ensures(p.E.tok, true, CanCallAssumption(p.E, etran), errorMessage, comment));
+          AddEnsures(ens, Ensures(p.E.tok, true, CanCallAssumption(p.E, etran), errorMessage, comment, null));
           comment = null;
           foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) {
             var post = s.E;
@@ -1464,16 +1464,16 @@ public partial class Translator {
             } else if (s.IsOnlyChecked && !bodyKind) {
               // don't include in split
             } else {
-              AddEnsures(ens, Ensures(s.Tok, s.IsOnlyFree, post, errorMessage, null));
+              AddEnsures(ens, Ensures(s.Tok, s.IsOnlyFree, post, errorMessage, null, s.Expr));
             }
           }
         }
         if (m is Constructor && kind == MethodTranslationKind.Call) {
           var fresh = Boogie.Expr.Not(etran.Old.IsAlloced(m.tok, new Boogie.IdentifierExpr(m.tok, "this", TrReceiverType(m))));
-          AddEnsures(ens, Ensures(m.tok, false, fresh, null, "constructor allocates the object"));
+          AddEnsures(ens, Ensures(m.tok, false, fresh, null, "constructor allocates the object", null));
         }
         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, ordinaryEtran.Old, ordinaryEtran, ordinaryEtran.Old)) {
-          AddEnsures(ens, Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
+          AddEnsures(ens, Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment, null));
         }
 
         // add the fuel assumption for the reveal method of a opaque method
@@ -1491,10 +1491,10 @@ public partial class Translator {
                 Boogie.Expr layer = etran.layerInterCluster.LayerN(1, moreFuel_expr);
                 Boogie.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr);
 
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuel, layer), null, null));
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuelAssert, layerAssert), null, null));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuel, layer), null, null, null));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuelAssert, layerAssert), null, null, null));
 
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr), null, "Shortcut to LZ"));
+                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr), null, "Shortcut to LZ", null));
               }
             }
           }
diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs
index 256dc2d73a4..3b45ce5d163 100644
--- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs
+++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs
@@ -555,14 +555,14 @@ public partial class Translator {
         var ss = TrSplitExpr(stmt.Expr, etran, true, out splitHappened);
         if (!splitHappened) {
           var tok = enclosingToken == null ? GetToken(stmt.Expr) : new NestedToken(enclosingToken, GetToken(stmt.Expr));
-          var desc = new PODesc.AssertStatement(errorMessage);
+          var desc = new PODesc.AssertStatement(errorMessage, stmt.Expr);
           (proofBuilder ?? b).Add(Assert(tok, etran.TrExpr(stmt.Expr), desc, stmt.Tok,
             etran.TrAttributes(stmt.Attributes, null)));
         } else {
           foreach (var split in ss) {
             if (split.IsChecked) {
               var tok = enclosingToken == null ? split.E.tok : new NestedToken(enclosingToken, split.Tok);
-              var desc = new PODesc.AssertStatement(errorMessage);
+              var desc = new PODesc.AssertStatement(errorMessage, split.Expr, true);
               (proofBuilder ?? b).Add(AssertNS(ToDafnyToken(tok), split.E, desc, stmt.Tok,
                 etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split
             }
diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index b535d475124..7dc566fe38c 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/Source/DafnyCore/Verifier/Translator.cs
@@ -1640,13 +1640,13 @@ void AddRedirectingTypeDeclAxioms<T>(bool is_alloc, T dd, string fullName)
             if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.Tok, currentModule)) {
               // this postcondition was inherited into this module, so just ignore it
             } else {
-              ens.Add(Ensures(s.Tok, s.IsOnlyFree, s.E, null, comment));
+              ens.Add(Ensures(s.Tok, s.IsOnlyFree, s.E, null, comment, s.Expr));
               comment = null;
             }
           }
         }
         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, iter.AllowsAllocation, etran.Old, etran, etran.Old)) {
-          ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
+          ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment, null));
         }
       }
 
@@ -4227,7 +4227,7 @@ public enum StmtType { NONE, ASSERT, ASSUME };
         string errorMessage = CustomErrorMessage(p.Attributes);
         foreach (var s in splits) {
           if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) {
-            AddEnsures(ens, Ensures(s.Tok, false, s.E, errorMessage, null));
+            AddEnsures(ens, Ensures(s.Tok, false, s.E, errorMessage, null, s.Expr));
           }
         }
       }
@@ -4272,7 +4272,7 @@ public enum StmtType { NONE, ASSERT, ASSUME };
         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(new Expression[] { e }, "default value", "in the two-state function's previous state");
             builder.Add(Assert(GetToken(e), wh, desc));
           }
         }
@@ -4520,7 +4520,7 @@ public enum StmtType { NONE, ASSERT, ASSUME };
         var witness = Zero(decl.tok, decl.Var.Type);
         if (witness == null) {
           witnessString = "";
-          witnessCheckBuilder.Add(Assert(decl.tok, Bpl.Expr.False, new PODesc.WitnessCheck(witnessString)));
+          witnessCheckBuilder.Add(Assert(decl.tok, Bpl.Expr.False, new PODesc.WitnessCheck(witnessString, decl, decl.Witness)));
         } else {
           // before trying 0 as a witness, check that 0 can be assigned to decl.Var
           witnessString = Printer.ExprToString(options, witness);
@@ -4535,7 +4535,7 @@ public enum StmtType { NONE, ASSERT, ASSUME };
 
         bool splitHappened;
         var ss = TrSplitExpr(witnessExpr, etran, true, out splitHappened);
-        var desc = new PODesc.WitnessCheck(witnessString);
+        var desc = new PODesc.WitnessCheck(witnessString, decl, witnessExpr);
         if (!splitHappened) {
           witnessCheckBuilder.Add(Assert(witnessCheckTok, etran.TrExpr(witnessExpr), desc));
         } else {
@@ -5242,9 +5242,11 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
       } 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(new[] { e }, "target object"), kv));
         if (!options.CommonHeapUse) {
-          builder.Add(Assert(tok, MkIsAlloc(etran.TrExpr(e), e.Type, etran.HeapExpr), new PODesc.IsAllocated("target object", null), kv));
+          builder.Add(Assert(tok, MkIsAlloc(etran.TrExpr(e), e.Type, etran.HeapExpr),
+            new PODesc.IsAllocated(new[] { e }, "target object", null), kv));
         }
       }
     }
@@ -5455,7 +5457,7 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
         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 (expr.Type.IsBigOrdinalType && !toType.IsBigOrdinalType) {
@@ -5466,7 +5468,8 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
 
       if (toType.IsBitVectorType) {
         var toWidth = toType.AsBitVectorType.Width;
-        var toBound = BaseTypes.BigNum.FromBigInt(BigInteger.One << toWidth);  // 1 << toWidth
+        var toBoundBigInteger = BigInteger.One << toWidth;
+        var toBound = BaseTypes.BigNum.FromBigInt(toBoundBigInteger);  // 1 << toWidth
         Bpl.Expr boundsCheck = null;
         if (expr.Type.IsBitVectorType) {
           var fromWidth = expr.Type.AsBitVectorType.Width;
@@ -5494,7 +5497,8 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
         }
 
         if (boundsCheck != null) {
-          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, errorMsgPrefix)));
+          builder.Add(Assert(tok, boundsCheck,
+            new PODesc.ConversionFit("value", toType, expr, toBoundBigInteger, errorMsgPrefix)));
         }
       }
 
@@ -5502,12 +5506,12 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
         if (expr.Type.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)));
+          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("value", toType, expr, 0, errorMsgPrefix)));
         } else if (expr.Type.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)));
+          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("real value", toType, expr, 0, errorMsgPrefix)));
         } else if (expr.Type.IsBitVectorType) {
           PutSourceIntoLocal();
           var fromWidth = expr.Type.AsBitVectorType.Width;
@@ -5518,7 +5522,7 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
             var toBound = BaseTypes.BigNum.FromBigInt(BigInteger.One << toWidth); // 1 << toWidth
             var bound = BplBvLiteralExpr(tok, toBound, expr.Type.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)));
+            builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("bit-vector value", toType, expr, toWidth, errorMsgPrefix)));
           }
         } else if (expr.Type.IsBigOrdinalType) {
           PutSourceIntoLocal();
@@ -5527,20 +5531,20 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
           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)));
+          builder.Add(Assert(tok, boundsCheck, new PODesc.ConversionFit("ORDINAL value", toType, expr, 0, errorMsgPrefix)));
         }
       } else if (toType.IsBigOrdinalType) {
         if (expr.Type.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 (expr.Type.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 desc = new PODesc.ConversionPositive("real", toType, expr, errorMsgPrefix);
           builder.Add(Assert(tok, boundsCheck, desc));
         }
       } else if (toType.IsNumericBased(Type.NumericPersuasion.Int)) {
@@ -5599,8 +5603,10 @@ void CheckCasePatternShape<VT>(CasePattern<VT> pat, Bpl.Expr rhs, IToken rhsTok,
         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, substMap, typeMap);
+        var constraint = etran.TrExpr(dafnyConstraint);
+        builder.Add(Assert(tok, constraint,
+          new PODesc.ConversionSatisfiesConstraints(errorMsgPrefix, kind, rdt.Name, dafnyConstraint)));
       }
     }
 
@@ -7258,13 +7264,13 @@ public ForceCheckToken(IToken tok)
       }
     }
 
-    Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment) {
+    Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment, Expression dafnyCondition) {
       Contract.Requires(tok != null);
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.Ensures>() != null);
 
       Bpl.Ensures ens = new Bpl.Ensures(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      ens.Description = new PODesc.AssertStatement(errorMessage ?? "this is the postcondition that could not be proved");
+      ens.Description = new PODesc.AssertStatement(errorMessage ?? "this is the postcondition that could not be proved", free ? null : dafnyCondition);
       return ens;
     }
 
@@ -7273,7 +7279,7 @@ public ForceCheckToken(IToken tok)
       Contract.Requires(condition != null);
       Contract.Ensures(Contract.Result<Bpl.Requires>() != null);
       Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);
-      req.Description = new PODesc.AssertStatement(errorMessage ?? "this is the precondition that could not be proved");
+      req.Description = new PODesc.AssertStatement(errorMessage ?? "this is the precondition that could not be proved", null);
       return req;
     }
 
@@ -7363,7 +7369,7 @@ public ForceCheckToken(IToken tok)
         }
         w = BplOr(body, w);
       }
-      builder.Add(Assert(tok, w, new PODesc.LetSuchThanExists()));
+      builder.Add(Assert(tok, w, new PODesc.LetSuchThatExists(bvars, expr)));
     }
 
     private void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListBuilder builder, BoogieStmtListBuilder builderOutsideIfConstruct, List<Variable> locals, ExpressionTranslator etran, bool isGhost) {
@@ -7844,6 +7850,9 @@ public ForceCheckToken(IToken tok)
         // the call site is inherited but all the context decreases expressions are new
         tok = new ForceCheckToken(tok);
       }
+
+      var calleeDecreasesFinal = new List<Expression>();
+      var contextDecreasesFinal = new List<Expression>();
       for (int i = 0; i < N; i++) {
         Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap, typeMap);
         Expression e1 = contextDecreases[i];
@@ -7854,6 +7863,8 @@ public ForceCheckToken(IToken tok)
         toks.Add(new NestedToken(tok, e1.tok));
         types0.Add(e0.Type.NormalizeExpand());
         types1.Add(e1.Type.NormalizeExpand());
+        calleeDecreasesFinal.Add(e0);
+        contextDecreasesFinal.Add(e1);
         callee.Add(etranCurrent.TrExpr(e0));
         caller.Add(etranInitial.TrExpr(e1));
       }
@@ -7862,7 +7873,8 @@ public ForceCheckToken(IToken tok)
       if (allowance != null) {
         decrExpr = Bpl.Expr.Or(allowance, decrExpr);
       }
-      builder.Add(Assert(tok, decrExpr, new PODesc.Terminates(inferredDecreases, false, hint)));
+      builder.Add(Assert(tok, decrExpr, new PODesc.Terminates(
+        contextDecreasesFinal, calleeDecreasesFinal, inferredDecreases, false, hint)));
     }
 
     /// <summary>
@@ -7907,20 +7919,24 @@ public ForceCheckToken(IToken tok)
           };
 
           Bpl.Expr zero = null;
+          Expression zeroDafny = null;
           string zeroStr = null;
           if (types0[k].IsNumericBased(Type.NumericPersuasion.Int)) {
             zero = Bpl.Expr.Literal(0);
             zeroStr = "0";
+            zeroDafny = new LiteralExpr(Token.NoToken, 0);
           } else if (types0[k].IsNumericBased(Type.NumericPersuasion.Real)) {
             zero = Bpl.Expr.Literal(BaseTypes.BigDec.ZERO);
             zeroStr = "0.0";
+            zeroDafny = new LiteralExpr(Token.NoToken, BigDec.FromInt(0));
           }
           if (zero != null) {
             Bpl.Expr bounded = Bpl.Expr.Le(zero, ee1[k]);
             for (int i = 0; i < k; i++) {
               bounded = Bpl.Expr.Or(bounded, Less[i]);
             }
-            Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), new PODesc.DecreasesBoundedBelow(N, k, zeroStr, suffixMsg));
+            Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]),
+              new PODesc.DecreasesBoundedBelow(N, k, zeroStr, zeroDafny, suffixMsg));
             builder.Add(cmd);
           }
         }
@@ -9872,11 +9888,13 @@ public enum K { Free, Checked, Both }
       public bool IsChecked { get { return Kind != K.Free; } }
       public readonly Expr E;
       public IToken Tok => ToDafnyToken(E.tok);
-      public SplitExprInfo(K kind, Expr e) {
+      public readonly Expression Expr;
+      public SplitExprInfo(K kind, Expr e, Expression expression) {
         Contract.Requires(e != null && e.tok != null);
         // TODO:  Contract.Requires(kind == K.Free || e.tok.IsValid);
         Kind = kind;
         E = e;
+        Expr = expression;
       }
     }
 
@@ -9981,7 +9999,8 @@ public enum K { Free, Checked, Both }
             var ss = new List<SplitExprInfo>();
             if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
               foreach (var s in ss) {
-                splits.Add(new SplitExprInfo(s.Kind, CondApplyBox(s.Tok, s.E, bce.FromType, bce.ToType)));
+                splits.Add(new SplitExprInfo(s.Kind,
+              CondApplyBox(s.Tok, s.E, bce.FromType, bce.ToType), null));
               }
               return true;
             }
@@ -10012,7 +10031,10 @@ public enum K { Free, Checked, Both }
                 etran.LayerOffset(1).TrLetExprPieces(e, out lhss, out rhss);
                 foreach (var s in ss) {
                   // as the source location in the following let, use that of the translated "s"
-                  splits.Add(new SplitExprInfo(s.Kind, new Bpl.LetExpr(s.E.tok, lhss, rhss, null, s.E)));
+                  splits.Add(new SplitExprInfo(s.Kind,
+              new Bpl.LetExpr(s.E.tok, lhss, rhss, null, s.E),
+                s.Expr != null ? new LetExpr(e.tok, e.LHSs, e.RHSs, s.Expr, true) : null
+              ));
                 }
                 return true;
               }
@@ -10041,7 +10063,10 @@ public enum K { Free, Checked, Both }
               var ss = new List<SplitExprInfo>();
               if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) {
                 foreach (var s in ss) {
-                  splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
+                  splits.Add(new SplitExprInfo(s.Kind,
+                Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E),
+                  s.Expr != null ? new UnaryOpExpr(s.E.tok, UnaryOpExpr.Opcode.Not, s.Expr) : null
+                ));
                 }
                 return true;
               }
@@ -10069,7 +10094,10 @@ public enum K { Free, Checked, Both }
                 TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
                 foreach (var s in ss) {
                   // as the source location in the following implication, use that of the translated "s"
-                  splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E)));
+                  splits.Add(new SplitExprInfo(s.Kind,
+              Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E),
+                s.Expr != null ? new BinaryExpr(s.E.tok, BinaryExpr.Opcode.Imp, bin.E0, s.Expr) : null
+              ));
                 }
               } else {
                 var ss = new List<SplitExprInfo>();
@@ -10077,7 +10105,10 @@ public enum K { Free, Checked, Both }
                 var rhs = etran.TrExpr(bin.E1);
                 foreach (var s in ss) {
                   // as the source location in the following implication, use that of the translated "s"
-                  splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
+                  splits.Add(new SplitExprInfo(s.Kind,
+                Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs),
+                  s.Expr != null ? new BinaryExpr(s.E.tok, BinaryExpr.Opcode.Imp, s.Expr, bin.E1) : null
+                ));
                 }
               }
               return true;
@@ -10127,7 +10158,7 @@ public enum K { Free, Checked, Both }
               foreach (var c in CoPrefixEquality(tok, codecl, e1type.TypeArgs, e2type.TypeArgs, kMinusOne, layer, A2, B2, true)) {
                 eqComponents = BplAnd(eqComponents, c);
                 var p = Bpl.Expr.Binary(c.tok, BinaryOperator.Opcode.Or, prefixEqK, Bpl.Expr.Imp(kHasSuccessor, c));
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p, null));
               }
               if (e.E0.Type.IsBigOrdinalType) {
                 var kIsNonZeroLimit = BplAnd(
@@ -10135,9 +10166,9 @@ public enum K { Free, Checked, Both }
                   FunctionCall(k.tok, "ORD#IsLimit", Bpl.Type.Bool, k));
                 var eq = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, null, etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), A, B);
                 var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Or, prefixEqK, BplOr(BplImp(kHasSuccessor, eqComponents), Bpl.Expr.Imp(kIsNonZeroLimit, eq)));
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p, null));
               }
-              splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, prefixEqK));
+              splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, prefixEqK, null));
               return true;
             }
 
@@ -10153,16 +10184,24 @@ public enum K { Free, Checked, Both }
             TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
 
             var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And;
+            var opExpr = position ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.And;
             var test = etran.TrExpr(ite.Test);
             foreach (var s in ssThen) {
               // as the source location in the following implication, use that of the translated "s"
-              splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, op, test, s.E)));
+              splits.Add(new SplitExprInfo(s.Kind,
+                Bpl.Expr.Binary(s.E.tok, op, test, s.E),
+                  s.Expr != null ? new BinaryExpr(s.E.tok, opExpr, ite.Test, s.Expr) : null
+                ));
             }
 
             var negatedTest = Bpl.Expr.Not(test);
+            var negatedTestExpr = new UnaryOpExpr(ite.Test.tok, UnaryOpExpr.Opcode.Not, ite.Test);
             foreach (var s in ssElse) {
               // as the source location in the following implication, use that of the translated "s"
-              splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, op, negatedTest, s.E)));
+              splits.Add(new SplitExprInfo(s.Kind,
+                Bpl.Expr.Binary(s.E.tok, op, negatedTest, s.E),
+                    s.Expr != null ? new BinaryExpr(s.E.tok, opExpr, negatedTestExpr, s.Expr) : null
+                ));
             }
 
             return true;
@@ -10178,12 +10217,16 @@ public enum K { Free, Checked, Both }
             // this assumption is not generated in non-split positions (because I don't know how.)
             // So, treat "S; E" like "SConclusion ==> E".
             if (position) {
-              var conclusion = etran.TrExpr(e.GetSConclusion());
+              var conclusionExpr = e.GetSConclusion();
+              var conclusion = etran.TrExpr(conclusionExpr);
               var ss = new List<SplitExprInfo>();
               TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran);
               foreach (var s in ss) {
                 // as the source location in the following implication, use that of the translated "s"
-                splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E)));
+                splits.Add(new SplitExprInfo(s.Kind,
+              Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E),
+                s.Expr != null ? new BinaryExpr(s.E.tok, BinaryExpr.Opcode.Imp, conclusionExpr, s.Expr) : null
+              ));
               }
             } else {
               var ss = new List<SplitExprInfo>();
@@ -10191,7 +10234,10 @@ public enum K { Free, Checked, Both }
               var rhs = etran.TrExpr(e.E);
               foreach (var s in ss) {
                 // as the source location in the following implication, use that of the translated "s"
-                splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs)));
+                splits.Add(new SplitExprInfo(s.Kind,
+              Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs),
+                s.Expr != null ? new BinaryExpr(s.E.tok, BinaryExpr.Opcode.Imp, s.Expr, e.E) : null
+              ));
               }
             }
             return true;
@@ -10288,7 +10334,8 @@ public enum K { Free, Checked, Both }
                 foreach (var kase in caseProduct) {
                   var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);
                   var etranBody = etran.LayerOffset(1);
-                  var bdy = etranBody.TrExpr(e.LogicalBody());
+                  var logicalBodyExpr = e.LogicalBody();
+                  var bdy = etranBody.TrExpr(logicalBodyExpr);
                   Bpl.Expr q;
                   var trig = TrTrigger(etranBody, e.Attributes, expr.tok);
                   if (position) {
@@ -10296,11 +10343,11 @@ public enum K { Free, Checked, Both }
                   } else {
                     q = new Bpl.ExistsExpr(kase.tok, bvars, trig, Bpl.Expr.And(ante, bdy));
                   }
-                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, q));
+                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, q, null));
                 }
 
                 // Finally, assume the original quantifier (forall/exists n :: P(n))
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr)));
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr), expr));
                 return true;
               } else {
                 // Don't use induction on these quantifiers.
@@ -10314,11 +10361,11 @@ public enum K { Free, Checked, Both }
                 }
                 if (etranBoost.Statistics_CustomLayerFunctionCount == 0) {
                   // apparently, the LayerOffset(1) we did had no effect
-                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, r));
+                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, r, expr));
                   return needsTokenAdjustment;
                 } else {
-                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, r));  // check the boosted expression
-                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr)));  // assume the ordinary expression
+                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, r, expr));  // check the boosted expression
+                  splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etran.TrExpr(expr), expr));  // assume the ordinary expression
                   return true;
                 }
               }
@@ -10334,11 +10381,11 @@ public enum K { Free, Checked, Both }
               }
               if (etran.Statistics_CustomLayerFunctionCount == 0) {
                 // apparently, doesn't use layer
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, r));
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, r, expr));
                 return needsTokenAdjustment;
               } else {
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, r));  // check the ordinary expression
-                splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etranBoost.TrExpr(expr)));  // assume the boosted expression
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, r, expr));  // check the ordinary expression
+                splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, etranBoost.TrExpr(expr), expr));  // assume the boosted expression
                 return true;
               }
             }
@@ -10361,7 +10408,7 @@ public enum K { Free, Checked, Both }
         translatedExpression.tok = new ForceCheckToken(expr.tok);
         splitHappened = true;
       }
-      splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, translatedExpression));
+      splits.Add(new SplitExprInfo(SplitExprInfo.K.Both, translatedExpression, expr));
       return splitHappened;
     }
 
@@ -10411,7 +10458,8 @@ public enum K { Free, Checked, Both }
             reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call are not inlined.");
             // F#canCall(args) ==> F(args)
             var p = Bpl.Expr.Binary(fargs.tok, BinaryOperator.Opcode.Imp, canCall, fargs);
-            splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p));
+            splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p,
+              new BinaryExpr((fargs.tok, BinaryExpr.Opcode.Imp, canCallExpr, fexp))));
             // F#canCall(args) && F(args)
             var fr = Bpl.Expr.And(canCall, fargs);
             splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr));
diff --git a/Source/DafnyPipeline.Test/TranslatorTest.cs b/Source/DafnyPipeline.Test/TranslatorTest.cs
index da4f100b719..7ac5d1579db 100644
--- a/Source/DafnyPipeline.Test/TranslatorTest.cs
+++ b/Source/DafnyPipeline.Test/TranslatorTest.cs
@@ -60,4 +60,305 @@ public class TranslatorTest {
     var forallFalseImpliesSomething = new Bpl.ForallExpr(nt, new List<Bpl.TypeVariable>(), new List<Bpl.Variable>(), Bpl.Expr.Imp(@false, var));
     Expect(forallFalseImpliesSomething, isAlwaysTrue: yes, isAlwaysFalse: no);
   }
+
+  // Test of embedding code into proof obligation descriptions
+
+  [Fact]
+  public void DivisionByZero() {
+    ShouldHaveImplicitCode(@"
+method Test(x: int, y: int) returns (z: int) {
+  z := 2 / (x + y); // Here
+}
+", "x + y != 0");
+  }
+
+  [Fact]
+  public void FunctionPrecondition() {
+    ShouldHaveImplicitCode(@"
+method Test(x: int, y: int) returns (z: int) {
+  z := HasPrecond(x + y); // Here
+}
+function HasPrecond(k: int): int
+  requires k % 10 != 0
+{
+  120 / (k % 10)
+}
+", "(x + y) % 10 != 0");
+  }
+
+
+  [Fact]
+  public void ClosurePrecondition() {
+    ShouldHaveImplicitCode(@"
+method Test(x: int, y: int; HasPrecond: int --> int) returns (z: int) {
+  z := HasPrecond(x + y); // Here
+}
+", "HasPrecond.requires(x + y)");
+  }
+
+  [Fact]
+  public void CompilableAssignSuchThat() {
+    ShouldHaveImplicitCode(@"
+predicate P(x: int)
+ 
+function Test(x: int, z: int): int
+  requires P(z) && x <= z
+{
+  var b :| x <= b && P(b); // Here
+  b
+}
+", "forall x0, y0 :: x <= x0 && P(x0) && x <= y0 && P(y0) ==> x0 == y0");
+  }
+
+  [Fact]
+  public void AssignmentSuchThatShouldExist() {
+    ShouldHaveImplicitCode(@"
+predicate P(x: int)
+ 
+lemma PUnique(a: int)
+  ensures forall x, y | a <= x && a <= y :: P(x) == P(y) ==> x == y
+
+function Test(x: int): int
+{
+  PUnique(x);
+  var b :| x <= b && P(b); // Here
+  b
+}
+", "exists b :: x <= b && P(b)");
+  }
+
+  [Fact]
+  public void ArrayIndexOutOfRange() {
+    ShouldHaveImplicitCode(@"
+method Test(a: int -> seq<int>, i: int) {
+  var b := a(2)[i + 3]; // Here
+}
+", "0 <= i + 3 < |a(2)|");
+  }
+
+  [Fact]
+  public void ArraySliceLowerOutOfRange() {
+    ShouldHaveImplicitCode(@"
+method Test(a: int -> seq<int>, i: int) {
+  var b := a(2)[i + 3..]; // Here
+}
+", "0 <= i + 3 <= |a(2)|");
+  }
+
+  [Fact]
+  public void ArrayUpperOutOfRange() {
+    ShouldHaveImplicitCode(@"
+method Test(a: int -> seq<int>, i: int, j: int) {
+  var b := a(2)[j..i + 3]; // Here
+}
+", "j <= i + 3 <= |a(2)|");
+  }
+
+  [Fact]
+  public void SubsetTypeConstraint() {
+    ShouldHaveImplicitCode(@"
+function method increment(i: int): int
+  requires i > 0 { i + 1 }
+
+method Call(fn: int -> int) {
+    var x := fn(-1);
+}
+
+method Main() {
+  Call(increment); // here
+}
+", "forall i: int :: increment.requires(i)");
+  }
+
+  [Fact]
+  public void DecreasesClause() {
+    ShouldHaveImplicitCode(@"
+function F(i: nat): nat
+
+function Recursive(i: nat, j: nat): int
+{
+  if i == 0 then 0 else
+    Recursive(F(i) + F(i+1), F(j)) // Here
+}
+", "F(i) + F(i+1) < i || (F(i) + F(i+1) == i && F(j) < j)");
+  }
+
+  [Fact]
+  public void ElementNotInDomain() {
+    ShouldHaveImplicitCode(@"
+method Test(m: map<int, int>, x: int) {
+  var b := m[x + 2]; // Here
+}
+", "x + 2 in m");
+  }
+
+  [Fact]
+  public void WitnessCheck() {
+    ShouldHaveImplicitCode(@"
+function f(): int
+
+type GreaterThanF = x: int | x >= f() witness 5 // Here
+
+", "5 >= f()");
+  }
+
+  [Fact]
+  public void NonNull() {
+    ShouldHaveImplicitCode(@"
+class A {
+  var x: int;
+}
+method Test(a: int -> A?) {
+  var b := a(2).x;
+}
+", "a(2) != null");
+  }
+
+  [Fact]
+  public void Allocated() {
+    ShouldHaveImplicitCode(@"
+class C {
+  constructor() {}
+  var x: int
+}
+method f() {
+  var c := new C();
+  assert old(c.x == 1); // here
+}
+", "allocated(c)");
+  }
+
+  [Fact]
+  public void AsInt() {
+    ShouldHaveImplicitCode(@"
+function g(): real
+
+method f() {
+  var n := g() as int; // Here
+}
+", "g().Floor as real == g()");
+  }
+
+  [Fact]
+  public void FitBv() {
+    ShouldHaveImplicitCode(@"
+function g(): real
+
+method f(x: bv16) {
+  var y := x as bv8; // Here
+}
+", "x < (1 << 8)");
+  }
+
+  [Fact]
+  public void IntFitsChar() {
+    ShouldHaveImplicitCode(@"
+method f(x: int) {
+  var y := x as char; // Here
+}
+", "(0 <= x && x < 55296) || (57344 <= x && x < 1114112)");
+    var notUnicode = new DafnyOptions {
+      UnicodeOutput = false
+    };
+    ShouldHaveImplicitCode(@"
+method f(x: int) {
+  var y := x as char; // Here
+}
+", "0 <= x && x < 65536", notUnicode);
+  }
+
+  [Fact]
+  public void SeqDecreases() {
+    ShouldHaveImplicitCode(@"
+method f(x: seq<int>, y: seq<int>)
+  decreases x
+{
+  if |x| > 0 {
+    assert ;
+    f(y, x);
+  }
+}
+", "|y| < |x| && y == x[0..|y|]");
+  }
+
+
+  [Fact]
+  public void BoolDecreases() {
+    ShouldHaveImplicitCode(@"
+predicate P1(b: bool)
+predicate P2(b: bool)
+predicate P3(b: bool)
+
+method f(x: bool, y: bool, z: bool)
+  decreases x, y, z
+{
+  assert (!P1(x) && x) ||
+    (P1(x) == x && ((!P2(y) && y) || 
+    (P2(y) == y && (!P3(z) && z))));
+  f(P1(x), P2(y), P3(z));
+}
+", "(!P1(x) && x) || (P1(x) == x && ((!P2(y) && y) || (P2(y) == y && (!P3(z) && z))))");
+  }
+
+  [Fact]
+  public void DatatypeDecreases() {
+    ShouldHaveImplicitCode(@"
+datatype X = A(x: X) | B(x: X) | C
+
+function D(x: X): X
+
+function Test(x: X): int {
+  if x != C then
+    Test(D(x)) // Here
+  else
+    0
+}
+", "D(x) < x");
+  }
+
+  [Fact]
+  public void RealFitsChar() {
+    ShouldHaveImplicitCode(@"
+method f(x: real)
+  requires x.Floor as real == x
+{
+  var y := x as char; // Here
+}
+", "(0.0 <= x && x < 55296.0) || (57344.0 <= x && x < 1114112.0)");
+    var notUnicode = new DafnyOptions {
+      UnicodeOutput = false
+    };
+    ShouldHaveImplicitCode(@"
+method f(x: real)
+  requires x.Floor as real == x
+{
+  var y := x as char; // Here
+}
+", "0.0 <= x && x < 65536.0", notUnicode);
+  }
+
+  [Fact]
+  public void ToOrdinalNeedsPositive() {
+    ShouldHaveImplicitCode(@"
+method f(x: int)
+{
+  var y := x as ORDINAL; // Here
+}
+", "0 <= x");
+
+    ShouldHaveImplicitCode(@"
+method f(x: real)
+  requires x.Floor as real == x;
+{
+  var y := x as ORDINAL; // Here
+}
+", "0.0 <= x");
+  }
+
+  private void ShouldHaveImplicitCode(string program, string expected, DafnyOptions options = null) {
+    Assert.True(false);
+    // Parse, resolve and translate the program
+    // Verify that the assertion has a proof obligation with a code that,
+    // if printed, yield the given.
+  }
 }