From 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 28 Oct 2014 00:11:20 -0700
Subject: Fixed a bug in the Substituter for datatype update expressions.

---
 Test/dafny0/DatatypeUpdate.dfy        | 7 +++++++
 Test/dafny0/DatatypeUpdate.dfy.expect | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0')

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]
+}
diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 069e7767..52595bf9 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 3 verified, 0 errors
-- 
cgit v1.2.3