1 files changed, 20 insertions, 0 deletions
diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy b/Test/dafny0/DatatypeUpdateResolution.dfy
new file mode 100644
index 00000000..26142fa8
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype MyDataType = MyConstructor(myint:int, mybool:bool) 
+                    | MyOtherConstructor(otherbool:bool) 
+                    | MyNumericConstructor(42:int)
+datatype SomeOtherType = S_O_T(non_destructor: int)
+
+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)
+  requires foo.MyConstructor?
+  ensures abc == foo.(myint := x + 2)
+  ensures jkl == foo.(non_destructor := 5)      // error: 'non_destructor' is not a destructor in MyDataType
+  ensures jkl == foo.(mybool := true, 40 := 100, myint := 200)  // error: '40' is not a destructor
+{
+  abc := MyConstructor(x + 2, foo.mybool).(myint := x + 3);
+  abc := foo.(myint := x + 2, mybool := true).(mybool := false);  // allowed
+  def := MyOtherConstructor(!foo.mybool).(otherbool := true, otherbool := true);  // error: duplicated member
+  ghi := MyConstructor(2, false).(otherbool := true);  // allowed, and will generate verification error
+  jkl := foo.(42 := 7, otherbool := true);  // error: members are from different constructors
+}