Fixed a bug in the Substituter for datatype update expressions.

1 files changed, 7 insertions, 0 deletions

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 09f07dd3..7869fba3 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -21,3 +21,10 @@ method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:
 

     assert abc[myint := abc.myint - 2] == foo[myint := x];

 }

+

+// regression test (for a previous bug in the Translator.Substituter):

+datatype Dt = Ctor(x: int, y: bool)

+function F(d: Dt): Dt

+{

+  d[x := 5]

+}