summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug104.dfy.expect
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-11-04 16:27:42 -0800
committerGravatar qunyanm <unknown>2015-11-04 16:27:42 -0800
commitd3c778854c2dc792a2dfbd9c5b05d667d18fb4c4 (patch)
tree7c5c0554b13c19256b8bb8863188797f9ca047dc /Test/dafny4/Bug104.dfy.expect
parent2b7d31bb3e0276028a8bc50c4933ea60fed5fb60 (diff)
Fix issue 104. Use ResolvedExpression to compute subexpressions for
DatatypeUpdateExpr if ResovedExpression is not null.
Diffstat (limited to 'Test/dafny4/Bug104.dfy.expect')
-rw-r--r--Test/dafny4/Bug104.dfy.expect3
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/dafny4/Bug104.dfy.expect b/Test/dafny4/Bug104.dfy.expect
new file mode 100644
index 00000000..1cc43cbf
--- /dev/null
+++ b/Test/dafny4/Bug104.dfy.expect
@@ -0,0 +1,3 @@
+Bug104.dfy(10,7): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)
+
+Dafny program verifier finished with 2 verified, 0 errors