1 files changed, 23 insertions, 0 deletions
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl
index 629cb04c..6460232c 100644
--- a/Test/inline/test5.bpl
+++ b/Test/inline/test5.bpl
@@ -54,3 +54,26 @@ procedure mainC()
   call P(1);
   assert Mem[1] == 1;  // good
 }
+
+// -------------------------------------------------
+
+type ref;
+var xyz: ref;
+
+procedure xyzA();
+  modifies xyz;
+  ensures old(xyz) == xyz;
+
+procedure {:inline 1} xyzB()
+  modifies xyz;
+{
+  call xyzA();
+}
+
+procedure xyzMain()
+  modifies xyz;
+{
+  call xyzA();
+  assert old(xyz) == xyz;
+  call xyzB();
+}