summaryrefslogtreecommitdiff
path: root/Test/hofs/Underspecified.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/hofs/Underspecified.dfy.expect')
-rw-r--r--Test/hofs/Underspecified.dfy.expect5
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect
index 04394d78..a5970830 100644
--- a/Test/hofs/Underspecified.dfy.expect
+++ b/Test/hofs/Underspecified.dfy.expect
@@ -1,5 +1,8 @@
+Underspecified.dfy(6,6): Error: the type of this variable is underspecified
Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly
+Underspecified.dfy(7,6): Error: the type of this variable is underspecified
Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly
Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly
+Underspecified.dfy(8,6): Error: the type of this variable is underspecified
Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly
-4 resolution/type errors detected in Underspecified.dfy
+7 resolution/type errors detected in Underspecified.dfy