diff options
author | leino <unknown> | 2014-10-28 00:11:20 -0700 |
---|---|---|
committer | leino <unknown> | 2014-10-28 00:11:20 -0700 |
commit | 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 (patch) | |
tree | 26d6d8993567e707bfcc8acb9754745d3d98a5d0 /Test/dafny0 | |
parent | 23ab50b9c9ae5d9e2030e28259a17bfab33af732 (diff) |
Fixed a bug in the Substituter for datatype update expressions.
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy | 7 | ||||
-rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy.expect | 2 |
2 files changed, 8 insertions, 1 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]
+}
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
|