1 files changed, 78 insertions, 78 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer
index f4e2b981..51798f57 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -2,28 +2,28 @@
 Boogie program verifier finished with 0 verified, 0 errors
 
 Boogie program verifier finished with 0 verified, 0 errors
-Triggers0.bpl(14,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
+Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
 1 parse errors detected in Triggers0.bpl
-Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(15,9): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(19,10): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(23,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(27,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(32,17): Error: equality is not allowed in triggers
-Triggers1.bpl(36,17): Error: arithmetic comparisons are not allowed in triggers
-Triggers1.bpl(45,10): Error: quantifiers are not allowed in triggers
-Triggers1.bpl(53,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(61,7): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(62,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(70,9): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g
-Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1
-Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0
+Triggers1.bpl(9,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(13,21): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(17,9): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(21,10): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(25,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(29,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(34,17): Error: equality is not allowed in triggers
+Triggers1.bpl(38,17): Error: arithmetic comparisons are not allowed in triggers
+Triggers1.bpl(47,10): Error: quantifiers are not allowed in triggers
+Triggers1.bpl(55,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(63,7): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(64,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(72,9): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(84,7): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(96,16): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(97,16): Error: a matching pattern must be more than just a variable by itself: g
+Triggers1.bpl(107,40): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(121,33): Error: cannot refer to a global variable in this context: h1
+Triggers1.bpl(122,33): Error: cannot refer to a global variable in this context: h0
 20 name resolution errors detected in Triggers1.bpl
 const x: int;
 
@@ -120,50 +120,50 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x
 Boogie program verifier finished with 0 verified, 0 errors
 
 Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
 2 type checking errors detected in Arrays1.bpl
-Types0.bpl(6,18): error: expected identifier before ':'
-Types0.bpl(6,12): error: expecting an identifier as parameter name
+Types0.bpl(8,18): error: expected identifier before ':'
+Types0.bpl(8,12): error: expecting an identifier as parameter name
 2 parse errors detected in Types0.bpl
-Types1.bpl(6,11): Error: undeclared type: x
-Types1.bpl(7,11): Error: undeclared type: x
-Types1.bpl(7,14): Error: undeclared type: x
+Types1.bpl(8,11): Error: undeclared type: x
+Types1.bpl(9,11): Error: undeclared type: x
+Types1.bpl(9,14): Error: undeclared type: x
 3 name resolution errors detected in Types1.bpl
-WhereParsing.bpl(14,37): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(15,33): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(32,38): error: attributes are not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(16,37): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(17,33): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(34,38): error: attributes are not allowed on the 'implementation' copies of formals
 3 parse errors detected in WhereParsing.bpl
-WhereParsing0.bpl(17,38): error: where clause not allowed on bound variables
-WhereParsing0.bpl(18,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(19,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(20,38): error: where clause not allowed on bound variables
 2 parse errors detected in WhereParsing0.bpl
-WhereParsing1.bpl(14,27): error: ")" expected
+WhereParsing1.bpl(16,27): error: ")" expected
 1 parse errors detected in WhereParsing1.bpl
-WhereParsing2.bpl(1,14): error: ";" expected
+WhereParsing2.bpl(3,14): error: ";" expected
 1 parse errors detected in WhereParsing2.bpl
-WhereResolution.bpl(28,38): Error: undeclared identifier: alpha
-WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts
+WhereResolution.bpl(30,38): Error: undeclared identifier: alpha
+WhereResolution.bpl(34,30): Error: old expressions allowed only in two-state contexts
 2 name resolution errors detected in WhereResolution.bpl
-BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
-BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
+BadLabels0.bpl(6,2): Error: more than one declaration of block name: X
+BadLabels0.bpl(13,4): Error: more than one declaration of block name: Y
 2 name resolution errors detected in BadLabels0.bpl
-BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined
-BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined
-BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
-BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
-BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
-BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
-BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
-BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
+BadLabels1.bpl(6,3): error: Error: goto label 'X' is undefined
+BadLabels1.bpl(7,3): error: Error: goto label 'Y' is undefined
+BadLabels1.bpl(49,3): error: Error: break statement is not inside a loop
+BadLabels1.bpl(51,5): error: Error: break statement is not inside a loop
+BadLabels1.bpl(62,5): error: Error: break label 'B' must designate an enclosing statement
+BadLabels1.bpl(65,5): error: Error: break label 'A' must designate an enclosing statement
+BadLabels1.bpl(66,5): error: Error: break label 'C' must designate an enclosing statement
+BadLabels1.bpl(67,8): error: Error: break label 'F' must designate an enclosing statement
 8 parse errors detected in BadLabels1.bpl
-LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
-LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(4,0): error: Malformed (#line num [filename]) pragma: #line
 LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is    No, I don't    well, it's an error is what it is
 LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }}  // error: A B C . txt(12,0)
 LineParse.bpl(6,2): error: EOF expected
 5 parse errors detected in LineParse.bpl
-LineResolve.bpl(5,1): Error: undeclared identifier: a
-LineResolve.bpl(7,2): Error: undeclared identifier: b
+LineResolve.bpl(7,1): Error: undeclared identifier: a
+LineResolve.bpl(9,2): Error: undeclared identifier: b
 LineResolve.bpl(12,0): Error: undeclared identifier: c
 LineResolve.bpl(13,10): Error: undeclared identifier: d
 LineResolve.bpl(12,0): Error: undeclared identifier: e
@@ -175,15 +175,15 @@ Abc.txt(99,0): Error: undeclared identifier: j
 c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
 A B C . txt(12,0): Error: undeclared identifier: l
 12 name resolution errors detected in LineResolve.bpl
-AttributeParsingErr.bpl(1,33): error: only attributes, not triggers, allowed here
 AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(5,52): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(7,37): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(9,31): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(11,29): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(13,13): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(15,18): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(20,26): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(5,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(7,52): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(9,37): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(11,31): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(13,29): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(15,13): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(17,18): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(22,26): error: only attributes, not triggers, allowed here
 9 parse errors detected in AttributeParsingErr.bpl
 
 type {:sourcefile "test.ssc"} T;
@@ -231,15 +231,15 @@ procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();
 const again: int;
 
 Boogie program verifier finished with 0 verified, 0 errors
-AttributeResolution.bpl(1,18): Error: undeclared identifier: foo
-AttributeResolution.bpl(3,18): Error: undeclared identifier: bar
-AttributeResolution.bpl(7,15): Error: undeclared identifier: qux
-AttributeResolution.bpl(7,41): Error: undeclared identifier: ij
-AttributeResolution.bpl(13,21): Error: undeclared identifier: bzzt
-AttributeResolution.bpl(15,20): Error: undeclared identifier: blt
-AttributeResolution.bpl(5,20): Error: undeclared identifier: baz
-AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
-AttributeResolution.bpl(11,29): Error: undeclared identifier: fux
+AttributeResolution.bpl(3,18): Error: undeclared identifier: foo
+AttributeResolution.bpl(5,18): Error: undeclared identifier: bar
+AttributeResolution.bpl(9,15): Error: undeclared identifier: qux
+AttributeResolution.bpl(9,41): Error: undeclared identifier: ij
+AttributeResolution.bpl(15,21): Error: undeclared identifier: bzzt
+AttributeResolution.bpl(17,20): Error: undeclared identifier: blt
+AttributeResolution.bpl(7,20): Error: undeclared identifier: baz
+AttributeResolution.bpl(11,18): Error: undeclared identifier: mux
+AttributeResolution.bpl(13,29): Error: undeclared identifier: fux
 9 name resolution errors detected in AttributeResolution.bpl
 
 function \true() : bool;
@@ -278,24 +278,24 @@ implementation qux(a: \procedure)
 Boogie program verifier finished with 0 verified, 0 errors
 
 Boogie program verifier finished with 0 verified, 0 errors
-MapsResolutionErrors.bpl(6,9): Error: type variable must occur in map arguments: b
-MapsResolutionErrors.bpl(20,10): Error: type variable must occur in procedure arguments: a
+MapsResolutionErrors.bpl(8,9): Error: type variable must occur in map arguments: b
+MapsResolutionErrors.bpl(22,10): Error: type variable must occur in procedure arguments: a
 2 name resolution errors detected in MapsResolutionErrors.bpl
-Orderings.bpl(12,20): Error: undeclared identifier: x
-Orderings.bpl(15,23): Error: c0 occurs more than once as parent
-Orderings.bpl(16,19): Error: constant cannot be its own parent
-Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
+Orderings.bpl(14,20): Error: undeclared identifier: x
+Orderings.bpl(17,23): Error: c0 occurs more than once as parent
+Orderings.bpl(18,19): Error: constant cannot be its own parent
+Orderings.bpl(20,20): Error: the parent of a constant has to be a constant
 4 name resolution errors detected in Orderings.bpl
-BadQuantifier.bpl(3,15): error: invalid QuantifierBody
+BadQuantifier.bpl(5,15): error: invalid QuantifierBody
 1 parse errors detected in BadQuantifier.bpl
 
 Boogie program verifier finished with 0 verified, 0 errors
 ----- SeparateVerification0.bpl
-SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
+SeparateVerification0.bpl(19,6): Error: undeclared identifier: y
 1 name resolution errors detected in SeparateVerification0.bpl
 ----- SeparateVerification1.bpl SeparateVerification0.bpl
-SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
-SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
+SeparateVerification1.bpl(6,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(16,6): Error: undeclared identifier: x
 2 name resolution errors detected in SeparateVerification0.bpl
 ----- SeparateVerification0.bpl SeparateVerification0.bpl