4 files changed, 20 insertions, 20 deletions
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/BindingGuards.dfy
index 0706fc5b..0706fc5b 100644
--- a/Test/dafny0/ExistentialGuards.dfy
+++ b/Test/dafny0/BindingGuards.dfy
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/BindingGuards.dfy.expect
index 65e9f179..b7da7b9e 100644
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ b/Test/dafny0/BindingGuards.dfy.expect
@@ -1,4 +1,4 @@
-// ExistentialGuards.dfy
+// BindingGuards.dfy
 
 predicate P(n: int)
 {
@@ -156,26 +156,26 @@ method P3(m: int, n: int)
     case x :| m <= x < n && P(x) =>
   }
 }
-ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
-ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
+BindingGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+BindingGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
     (0,0): anon12_Then
     (0,0): anon9
     (0,0): anon16_Then
-ExistentialGuards.dfy(134,9): Error: assertion violation
-ExistentialGuards.dfy(6,8): Related location
+BindingGuards.dfy(134,9): Error: assertion violation
+BindingGuards.dfy(6,8): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon20_Then
     (0,0): anon21_Then
     (0,0): anon5
     (0,0): anon17
-ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
 Execution trace:
     (0,0): anon0
     (0,0): anon7_Else
-ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
+BindingGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
 Execution trace:
     (0,0): anon0
     (0,0): anon7_Else
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/BindingGuardsResolution.dfy
index e2b55a99..e2b55a99 100644
--- a/Test/dafny0/ExistentialGuardsResolution.dfy
+++ b/Test/dafny0/BindingGuardsResolution.dfy
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/BindingGuardsResolution.dfy.expect
index c9b62ff5..b6f23805 100644
--- a/Test/dafny0/ExistentialGuardsResolution.dfy.expect
+++ b/Test/dafny0/BindingGuardsResolution.dfy.expect
@@ -1,4 +1,4 @@
-// ExistentialGuardsResolution.dfy
+// BindingGuardsResolution.dfy
 
 
 module TypesNotFullyDetermined {
@@ -151,15 +151,15 @@ method P1(m: int, n: int)
     case m < n =>
   }
 }
-ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
-ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
-ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
-11 resolution/type errors detected in ExistentialGuardsResolution.dfy
+BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
+BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+BindingGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
+BindingGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
+11 resolution/type errors detected in BindingGuardsResolution.dfy