2 files changed, 73 insertions, 4 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1d1fc2d9..8f138bcd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2139,16 +2139,16 @@ Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
 
-Dafny program verifier finished with 19 verified, 2 errors
-out.tmp.dfy(10,12): Error: assertion violation
+Dafny program verifier finished with 28 verified, 2 errors
+out.tmp.dfy(66,12): Error: assertion violation
 Execution trace:
     (0,0): anon0
-out.tmp.dfy(101,21): Error: assertion violation
+out.tmp.dfy(157,21): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
 
-Dafny program verifier finished with 19 verified, 2 errors
+Dafny program verifier finished with 28 verified, 2 errors
 
 Dafny program verifier finished with 26 verified, 0 errors
 Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index cd712b7d..3947737b 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -147,3 +147,72 @@ function Theorem3(n: int): int
     var y := Theorem3(n-1);
     5
 }
+
+// ----- tricky substitution issues in the implementation -----
+
+class TrickySubstitution {
+  function F0(x: int): int
+    ensures F0(x) == x;
+  {
+    var g :| x == g;
+    g
+  }
+
+  function F1(x: int): int
+    ensures F1(x) == x;
+  {
+    var f := x;
+    var g :| f == g;
+    g
+  }
+
+  function F2(x: int): int
+    ensures F2(x) == x;
+  {
+    var f, g :| f == x && f == g;
+    g
+  }
+
+  function F3(x: int): int
+    ensures F3(x) == x;
+  {
+    var f :| f == x;
+    var g :| f == g;
+    g
+  }
+
+  var v: int;
+  var w: int;
+
+  function F4(x: int): int
+    requires this.v + x == 3 && this.w == 2;
+    reads this;
+    ensures F4(x) == 5;
+  {
+    var f := this.v + x;  // 3
+    var g :| f + this.w == g;  // 5
+    g
+  }
+
+  method M(x: int)
+    requires this.v + x == 3 && this.w == 2;
+    modifies this;
+  {
+    this.v := this.v + 1;
+    this.w := this.w + 10;
+    assert 6 ==
+      var f := this.v + x;  // 4
+      var g :| old(f + this.w) == g;  // 6
+      g;
+  }
+
+  method N() returns (ghost r: int, ghost s: int)
+    requires w == 12;
+    modifies this;
+    ensures r == 12 == s && w == 13;
+  {
+    w := w + 1;
+    r := var y :| y == old(w); y;
+    s := old(var y :| y == w; y);
+  }
+}