Merge

20 files changed, 1704 insertions, 1351 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index ae26d8db..746504b3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -594,6 +594,15 @@ namespace Microsoft.Boogie {
         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

 

+      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {

+        BlockPredicator.Predicate(program, false, false);

+        if (CommandLineOptions.Clo.PrintInstrumented) {

+          using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {

+            program.Emit(writer);

+          }

+        }

+      }

+

       Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

       if (CommandLineOptions.Clo.ExtractLoops)

       {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 7d55e177..e7633014 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -574,6 +574,8 @@ namespace Microsoft.Boogie {
     public string CoverageReporterPath = null;

     public Process coverageReporter = null; // used internally for debugging

 

+    public bool DoPredication = false;

+

     public enum TypeEncoding {

       None,

       Predicates,

@@ -1230,7 +1232,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

-              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

+              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||

+              ps.CheckBooleanFlag("predicate", ref DoPredication)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 66756b0c..4b9e0c27 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -290,10 +290,13 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
 ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>

 = (. IToken/*!*/ id;

      Attributes attrs = null;

+     var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

   .)

   "type"

   { Attribute<ref attrs> }

-  Ident<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

+  Ident<out id>

+  [ "(" "==" ")"               (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)

+  ]                            (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)

   SYNC ";"

   .

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

@@ -356,10 +359,16 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
 /*------------------------------------------------------------------------*/

 GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>

 = (. Contract.Requires(cce.NonNullElements(typeArgs));

-     IToken/*!*/ id; .)

+     IToken/*!*/ id;

+     TypeParameter.EqualitySupportValue eqSupport;

+  .)

   "<"

-  Ident<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)

-  { "," Ident<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)

+  Ident<out id>              (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)

+  [ "(" "==" ")"             (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)

+    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)

+  { "," Ident<out id>        (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)

+    [ "(" "==" ")"           (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)

+    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)

   }

   ">"

   .

@@ -1027,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
 /*------------------------------------------------------------------------*/

 AssertStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-     Expression/*!*/ e = null; Attributes attrs = null;

+     Expression e = null; Attributes attrs = null;

   .)

-  "assert"                                     (. x = t; s = null;.)

+  "assert"                                     (. x = t; .)

   { IF(IsAttribute()) Attribute<ref attrs> }

-  ( Expression<out e>                 

+  ( Expression<out e>

   | "..."

   )

   ";"

@@ -1043,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s>
   .)

   .

 AssumeStmt<out Statement/*!*/ s>

-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)

+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+     Expression e = null; Attributes attrs = null;

+  .)

   "assume"                                     (. x = t; .)

-  Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)

+  { IF(IsAttribute()) Attribute<ref attrs> }

+  ( Expression<out e>

+  | "..."

+  )

+  (. if (e == null) {

+       s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+     } else {

+       s = new AssumeStmt(x, e, attrs);

+     }

+  .)

+  ";"

   .

 PrintStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 5e6ad5c3..bf985ddc 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -269,8 +269,18 @@ namespace Microsoft.Dafny {
     }

     public bool IsTypeParameter {

       get {

+        return AsTypeParameter != null;

+      }

+    }

+    public TypeParameter AsTypeParameter {

+      get {

         UserDefinedType ct = this as UserDefinedType;

-        return ct != null && ct.ResolvedParam != null;

+        return ct == null ? null : ct.ResolvedParam;

+      }

+    }

+    public virtual bool SupportsEquality {

+      get {

+        return true;

       }

     }

   }

@@ -318,16 +328,20 @@ namespace Microsoft.Dafny {
 

   public abstract class CollectionType : NonProxyType

   {

-    public readonly Type Arg;

+    public readonly Type Arg;  // denotes the Domain type for a Map

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Arg != null);

     }

-

     public CollectionType(Type arg) {

       Contract.Requires(arg != null);

       this.Arg = arg;

     }

+    public override bool SupportsEquality {

+      get {

+        return Arg.SupportsEquality;

+      }

+    }

   }

 

   public class SetType : CollectionType {

@@ -369,12 +383,14 @@ namespace Microsoft.Dafny {
   }

   public class MapType : CollectionType

   {

-    public Type Domain, Range;

+    public Type Range;

     public MapType(Type domain, Type range) : base(domain) {

       Contract.Requires(domain != null && range != null);

-      Domain = domain;

       Range = range;

     }

+    public Type Domain {

+      get { return Arg; }

+    }

     [Pure]

     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

@@ -515,6 +531,35 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

+

+    public override bool SupportsEquality {

+      get {

+        if (ResolvedClass is ClassDecl) {

+          return true;

+        } else if (ResolvedClass is CoDatatypeDecl) {

+          return false;

+        } else if (ResolvedClass is IndDatatypeDecl) {

+          var dt = (IndDatatypeDecl)ResolvedClass;

+          Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);

+          if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {

+            return false;

+          }

+          Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count);

+          var i = 0;

+          foreach (var tp in dt.TypeArgs) {

+            if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) {

+              return false;

+            }

+            i++;

+          }

+          return true;

+        } else if (ResolvedParam != null) {

+          return ResolvedParam.MustSupportEquality;

+        }

+        Contract.Assume(false);  // the SupportsEquality getter requires the Type to have been successfully resolved

+        return true;

+      }

+    }

   }

 

   public abstract class TypeProxy : Type {

@@ -529,6 +574,15 @@ namespace Microsoft.Dafny {
       Contract.Assume(T == null || cce.IsPeerConsistent(T));

       return T == null ? "?" : T.ToString();

     }

+    public override bool SupportsEquality {

+      get {

+        if (T != null) {

+          return T.SupportsEquality;

+        } else {

+          return base.SupportsEquality;

+        }

+      }

+    }

   }

 

   public abstract class UnrestrictedTypeProxy : TypeProxy {

@@ -589,17 +643,6 @@ namespace Microsoft.Dafny {
   }

 

   /// <summary>

-  /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.

-  /// </summary>

-  public class ObjectsTypeProxy : RestrictedTypeProxy {

-    public override int OrderID {

-      get {

-        return 2;

-      }

-    }

-  }

-

-  /// <summary>

   /// This proxy stands for:

   ///     set(Arg) or seq(Arg) or map(Arg, Range)

   /// </summary>

@@ -616,7 +659,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 3;

+        return 2;

       }

     }

   }

@@ -635,7 +678,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 4;

+        return 3;

       }

     }

   }

@@ -658,7 +701,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 5;

+        return 4;

       }

     }

   }

@@ -723,10 +766,19 @@ namespace Microsoft.Dafny {
         parent = value;

       }

     }

-    public TypeParameter(IToken tok, string name)

+    public enum EqualitySupportValue { Required, InferredRequired, Unspecified }

+    public EqualitySupportValue EqualitySupport;  // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required)

+    public bool MustSupportEquality {

+      get { return EqualitySupport != EqualitySupportValue.Unspecified; }

+    }

+

+    public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false;  // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl

+

+    public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)

       : base(tok, name, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

+      EqualitySupport = equalitySupport;

     }

   }

 

@@ -888,7 +940,10 @@ namespace Microsoft.Dafny {
   public class IndDatatypeDecl : DatatypeDecl

   {

     public DatatypeCtor DefaultCtor;  // set during resolution

-    public bool[] TypeParametersUsedInConstructionByDefaultCtor;  // set during resolution; has same length as

+    public bool[] TypeParametersUsedInConstructionByDefaultCtor;  // set during resolution; has same length as the number of type arguments

+

+    public enum ES { NotYetComputed, Never, ConsultTypeArguments }

+    public ES EqualitySupport = ES.NotYetComputed;

 

     public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,

       [Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)

@@ -953,13 +1008,15 @@ namespace Microsoft.Dafny {
 

   public abstract class MemberDecl : Declaration {

     public readonly bool IsStatic;

+    public readonly bool IsGhost;

     public TopLevelDecl EnclosingClass;  // filled in during resolution

 

-    public MemberDecl(IToken tok, string name, bool isStatic, Attributes attributes)

+    public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       IsStatic = isStatic;

+      IsGhost = isGhost;

     }

     /// <summary>

     /// Returns className+"."+memberName.  Available only after resolution.

@@ -983,7 +1040,6 @@ namespace Microsoft.Dafny {
   }

 

   public class Field : MemberDecl {

-    public readonly bool IsGhost;

     public readonly bool IsMutable;

     public readonly Type Type;

     [ContractInvariantMethod]

@@ -999,11 +1055,10 @@ namespace Microsoft.Dafny {
     }

 

     public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)

-      : base(tok, name, false, attributes) {

+      : base(tok, name, false, isGhost, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(type != null);

-      IsGhost = isGhost;

       IsMutable = isMutable;

       Type = type;

     }

@@ -1043,17 +1098,23 @@ namespace Microsoft.Dafny {
   public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType

   {

     public readonly TypeParameter TheType;

+    public TypeParameter.EqualitySupportValue EqualitySupport {

+      get { return TheType.EqualitySupport; }

+    }

+    public bool MustSupportEquality {

+      get { return TheType.MustSupportEquality; }

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(TheType != null && Name == TheType.Name);

     }

 

-    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes)

+    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes)

       : base(tok, name, module, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

-      TheType = new TypeParameter(tok, name);

+      TheType = new TypeParameter(tok, name, equalitySupport);

     }

   }

 

@@ -1153,7 +1214,7 @@ namespace Microsoft.Dafny {
             return name + nm.Substring(i);

           }

         } else {

-          string nxt = nm.Substring(i, j);

+          string nxt = nm.Substring(i, j - i);

           name = name == null ? nxt : name + nxt;

           switch (nm[j]) {

             case '\'': name += "_k"; break;

@@ -1274,7 +1335,6 @@ namespace Microsoft.Dafny {
   }

 

   public class Function : MemberDecl, TypeParameter.ParentType {

-    public readonly bool IsGhost;  // functions are "ghost" by default; a non-ghost function is called a "function method"

     public bool IsRecursive;  // filled in during resolution

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals

@@ -1297,11 +1357,14 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Decreases != null);

     }

 

+    /// <summary>

+    /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".

+    /// </summary>

     public Function(IToken tok, string name, bool isStatic, bool isGhost,

                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,

                     List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                     Expression body, Attributes attributes, bool signatureOmitted)

-      : base(tok, name, isStatic, attributes) {

+      : base(tok, name, isStatic, isGhost, attributes) {

 

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1312,7 +1375,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(reads));

       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

-      this.IsGhost = isGhost;

       this.TypeArgs = typeArgs;

       this.OpenParen = openParen;

       this.Formals = formals;

@@ -1341,7 +1403,6 @@ namespace Microsoft.Dafny {
 

   public class Method : MemberDecl, TypeParameter.ParentType

   {

-    public readonly bool IsGhost;

     public readonly bool SignatureIsOmitted;

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly List<Formal/*!*/>/*!*/ Ins;

@@ -1372,7 +1433,7 @@ namespace Microsoft.Dafny {
                   [Captured] Specification<Expression>/*!*/ decreases,

                   [Captured] BlockStmt body,

                   Attributes attributes, bool signatureOmitted)

-      : base(tok, name, isStatic, attributes) {

+      : base(tok, name, isStatic, isGhost, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

@@ -1382,7 +1443,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(mod != null);

       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

-      this.IsGhost = isGhost;

       this.TypeArgs = typeArgs;

       this.Ins = ins;

       this.Outs = outs;

@@ -1507,60 +1567,40 @@ namespace Microsoft.Dafny {
 

   public abstract class PredicateStmt : Statement

   {

-    [Peer]

     public readonly Expression Expr;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr, Attributes attrs)

       : base(tok, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr)

       : this(tok, expr, null) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

   }

 

   public class AssertStmt : PredicateStmt {

-    [Captured]

     public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

       : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-    }

-

-    [Captured]

-    public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : this(tok, expr, null) {

-      Contract.Requires(tok != null);

-      Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

     }

   }

 

   public class AssumeStmt : PredicateStmt {

-    [Captured]

-    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : base(tok, expr) {

+    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

+      : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-

     }

   }

 

@@ -1640,6 +1680,18 @@ namespace Microsoft.Dafny {
       Attributes = attrs;

     }

     public abstract bool CanAffectPreviouslyKnownExpressions { get; }

+    /// <summary>

+    /// Returns the non-null subexpressions of the AssignmentRhs.

+    /// </summary>

+    public virtual IEnumerable<Expression> SubExpressions {

+      get { yield break; }

+    }

+    /// <summary>

+    /// Returns the non-null sub-statements of the AssignmentRhs.

+    /// </summary>

+    public virtual IEnumerable<Statement> SubStatements{

+      get { yield break; }

+    }

   }

 

   public class ExprRhs : AssignmentRhs

@@ -1657,6 +1709,11 @@ namespace Microsoft.Dafny {
       Expr = expr;

     }

     public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Expr;

+      }

+    }

   }

 

   public class TypeRhs : AssignmentRhs

@@ -1705,6 +1762,23 @@ namespace Microsoft.Dafny {
         return false;

       }

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        if (ArrayDimensions != null) {

+          foreach (var e in ArrayDimensions) {

+            yield return e;

+          }

+        }

+      }

+    }

+    public override IEnumerable<Statement> SubStatements {

+      get {

+        if (InitCall != null) {

+          yield return InitCall;

+        }

+      }

+    }

   }

 

   public class CallRhs : AssignmentRhs

@@ -1744,6 +1818,14 @@ namespace Microsoft.Dafny {
         return false;

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Receiver;

+        foreach (var e in Args) {

+          yield return e;

+        }

+      }

+    }

   }

 

   public class HavocRhs : AssignmentRhs {

@@ -1980,6 +2062,7 @@ namespace Microsoft.Dafny {
     public Expression/*!*/ Receiver;

     public readonly string/*!*/ MethodName;

     public readonly List<Expression/*!*/>/*!*/ Args;

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // create, initialized, and used by resolution (could be deleted once all of resolution is done)

     public Method Method;  // filled in by resolution

 

     public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,

@@ -2018,13 +2101,13 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Thn != null);

-      Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt);

+      Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt || Els is SkeletonStatement);

     }

     public IfStmt(IToken tok, Expression guard, BlockStmt thn, Statement els)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(thn != null);

-      Contract.Requires(els == null || els is BlockStmt || els is IfStmt);

+      Contract.Requires(els == null || els is BlockStmt || els is IfStmt || els is SkeletonStatement);

       this.Guard = guard;

       this.Thn = thn;

       this.Els = els;

@@ -2317,6 +2400,8 @@ namespace Microsoft.Dafny {
   ///   S == null

   /// * assert ...

   ///   ConditionOmitted == true

+  /// * assume ...

+  ///   ConditionOmitted == true

   /// * if ... { Stmt }

   ///   if ... { Stmt } else ElseStmt

   ///   ConditionOmitted == true

@@ -2785,6 +2870,7 @@ namespace Microsoft.Dafny {
     public readonly Expression/*!*/ Receiver;

     public readonly IToken OpenParen;  // can be null if Args.Count == 0

     public readonly List<Expression/*!*/>/*!*/ Args;

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // create, initialized, and used by resolution (could be deleted once all of resolution is done)

     public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }

     public CoCallResolution CoCall = CoCallResolution.No;  // indicates whether or not the call is a co-recursive call; filled in by resolution

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 26b98833..a4e51924 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -315,7 +315,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 22) {

+		if (la.kind == 25) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

@@ -351,7 +351,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 22) {

+		if (la.kind == 25) {

 			GenericParameters(typeArgs);

 		}

 		Expect(16);

@@ -376,13 +376,20 @@ bool IsAttribute() {
 	void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) {

 		IToken/*!*/ id;

 		Attributes attrs = null;

+		var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

 		

 		Expect(21);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		at = new ArbitraryTypeDecl(id, id.val, module, attrs); 

+		if (la.kind == 22) {

+			Get();

+			Expect(23);

+			Expect(24);

+			eqSupport = TypeParameter.EqualitySupportValue.Required; 

+		}

+		at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); 

 		while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();}

 		Expect(18);

 	}

@@ -405,10 +412,10 @@ bool IsAttribute() {
 		}

 		if (la.kind == 19) {

 			FieldDecl(mmod, mm);

-		} else if (la.kind == 44 || la.kind == 45) {

+		} else if (la.kind == 45 || la.kind == 46) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 24 || la.kind == 25) {

+		} else if (la.kind == 27 || la.kind == 28) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

 		} else SynErr(114);

@@ -416,16 +423,32 @@ bool IsAttribute() {
 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

 		Contract.Requires(cce.NonNullElements(typeArgs));

-		IToken/*!*/ id; 

-		Expect(22);

+		IToken/*!*/ id;

+		TypeParameter.EqualitySupportValue eqSupport;

+		

+		Expect(25);

 		Ident(out id);

-		typeArgs.Add(new TypeParameter(id, id.val)); 

+		eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

+		if (la.kind == 22) {

+			Get();

+			Expect(23);

+			Expect(24);

+			eqSupport = TypeParameter.EqualitySupportValue.Required; 

+		}

+		typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); 

 		while (la.kind == 20) {

 			Get();

 			Ident(out id);

-			typeArgs.Add(new TypeParameter(id, id.val)); 

+			eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

+			if (la.kind == 22) {

+				Get();

+				Expect(23);

+				Expect(24);

+				eqSupport = TypeParameter.EqualitySupportValue.Required; 

+			}

+			typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); 

 		}

-		Expect(23);

+		Expect(26);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -470,9 +493,9 @@ bool IsAttribute() {
 		IToken bodyEnd = Token.NoToken;

 		bool signatureOmitted = false;

 		

-		if (la.kind == 44) {

+		if (la.kind == 45) {

 			Get();

-			if (la.kind == 24) {

+			if (la.kind == 27) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -482,22 +505,22 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			Ident(out id);

-			if (la.kind == 22 || la.kind == 33) {

-				if (la.kind == 22) {

+			if (la.kind == 22 || la.kind == 25) {

+				if (la.kind == 25) {

 					GenericParameters(typeArgs);

 				}

 				Formals(true, isFunctionMethod, formals, out openParen);

 				Expect(5);

 				Type(out returnType);

-			} else if (la.kind == 27) {

+			} else if (la.kind == 30) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

 			} else SynErr(117);

-		} else if (la.kind == 45) {

+		} else if (la.kind == 46) {

 			Get();

 			isPredicate = true; 

-			if (la.kind == 24) {

+			if (la.kind == 27) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -508,17 +531,17 @@ bool IsAttribute() {
 			}

 			Ident(out id);

 			if (StartOf(4)) {

-				if (la.kind == 22) {

+				if (la.kind == 25) {

 					GenericParameters(typeArgs);

 				}

-				if (la.kind == 33) {

+				if (la.kind == 22) {

 					Formals(true, isFunctionMethod, formals, out openParen);

 					if (la.kind == 5) {

 						Get();

 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

-			} else if (la.kind == 27) {

+			} else if (la.kind == 30) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

@@ -562,10 +585,10 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();}

-		if (la.kind == 24) {

+		while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(120); Get();}

+		if (la.kind == 27) {

 			Get();

-		} else if (la.kind == 25) {

+		} else if (la.kind == 28) {

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

@@ -587,17 +610,17 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 22 || la.kind == 33) {

-			if (la.kind == 22) {

+		if (la.kind == 22 || la.kind == 25) {

+			if (la.kind == 25) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, !mmod.IsGhost, ins, out openParen);

-			if (la.kind == 26) {

+			if (la.kind == 29) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 				Formals(false, !mmod.IsGhost, outs, out openParen);

 			}

-		} else if (la.kind == 27) {

+		} else if (la.kind == 30) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

 		} else SynErr(122);

@@ -629,7 +652,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 22) {

 			FormalsOptionalIds(formals);

 		}

 		ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); 

@@ -637,7 +660,7 @@ bool IsAttribute() {
 

 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

-		Expect(33);

+		Expect(22);

 		if (StartOf(7)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

@@ -647,7 +670,7 @@ bool IsAttribute() {
 				formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			}

 		}

-		Expect(34);

+		Expect(24);

 	}

 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

@@ -731,22 +754,22 @@ bool IsAttribute() {
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 35: {

+		case 36: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 36: {

+		case 37: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 37: {

+		case 38: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 38: {

+		case 39: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -757,7 +780,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 39: {

+		case 40: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -768,7 +791,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 40: {

+		case 41: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -779,7 +802,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 41: {

+		case 42: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -790,7 +813,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 1: case 3: case 42: {

+		case 1: case 3: case 43: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

@@ -800,7 +823,7 @@ bool IsAttribute() {
 

 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

-		Expect(33);

+		Expect(22);

 		openParen = t; 

 		if (la.kind == 1 || la.kind == 8) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

@@ -811,7 +834,7 @@ bool IsAttribute() {
 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}

-		Expect(34);

+		Expect(24);

 	}

 

 	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

@@ -820,7 +843,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

 		while (!(StartOf(8))) {SynErr(124); Get();}

-		if (la.kind == 28) {

+		if (la.kind == 31) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

@@ -836,18 +859,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}

 			Expect(18);

-		} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {

-			if (la.kind == 29) {

+		} else if (la.kind == 32 || la.kind == 33 || la.kind == 34) {

+			if (la.kind == 32) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 30) {

+			if (la.kind == 33) {

 				Get();

 				Expression(out e);

 				while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}

 				Expect(18);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (la.kind == 31) {

+			} else if (la.kind == 34) {

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

@@ -857,7 +880,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Expect(18);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

 			} else SynErr(128);

-		} else if (la.kind == 32) {

+		} else if (la.kind == 35) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

@@ -885,7 +908,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void FrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; 

 		Expression(out e);

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -920,7 +943,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(22);

+		Expect(25);

 		Type(out ty);

 		gt.Add(ty); 

 		while (la.kind == 20) {

@@ -928,7 +951,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(23);

+		Expect(26);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -937,7 +960,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken moduleName = null;

 		List<Type/*!*/>/*!*/ gt;

 		

-		if (la.kind == 42) {

+		if (la.kind == 43) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 3) {

@@ -956,12 +979,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 1) {

 			Ident(out tok);

 			gt = new List<Type/*!*/>(); 

-			if (la.kind == 43) {

+			if (la.kind == 44) {

 				moduleName = tok; 

 				Get();

 				Ident(out tok);

 			}

-			if (la.kind == 22) {

+			if (la.kind == 25) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt, moduleName); 

@@ -971,14 +994,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

 		Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

-		if (la.kind == 30) {

-			while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();}

+		if (la.kind == 33) {

+			while (!(la.kind == 0 || la.kind == 33)) {SynErr(132); Get();}

 			Get();

 			Expression(out e);

 			while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}

 			Expect(18);

 			reqs.Add(e); 

-		} else if (la.kind == 46) {

+		} else if (la.kind == 47) {

 			Get();

 			if (StartOf(11)) {

 				PossiblyWildFrameExpression(out fe);

@@ -991,13 +1014,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();}

 			Expect(18);

-		} else if (la.kind == 31) {

+		} else if (la.kind == 34) {

 			Get();

 			Expression(out e);

 			while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();}

 			Expect(18);

 			ens.Add(e); 

-		} else if (la.kind == 32) {

+		} else if (la.kind == 35) {

 			Get();

 			DecreasesList(decreases, false);

 			while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();}

@@ -1016,7 +1039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(9)) {

@@ -1027,7 +1050,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void PossiblyWildExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);

 		e = dummyExpr; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			e = new WildcardExpr(t); 

 		} else if (StartOf(9)) {

@@ -1056,19 +1079,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = bs; 

 			break;

 		}

-		case 66: {

+		case 67: {

 			AssertStmt(out s);

 			break;

 		}

-		case 54: {

+		case 55: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 67: {

+		case 68: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 1: case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1076,23 +1099,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 59: {

+		case 60: {

 			IfStmt(out s);

 			break;

 		}

-		case 63: {

+		case 64: {

 			WhileStmt(out s);

 			break;

 		}

-		case 65: {

+		case 66: {

 			MatchStmt(out s);

 			break;

 		}

-		case 68: {

+		case 69: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 49: {

+		case 50: {

 			Get();

 			x = t; 

 			Ident(out id);

@@ -1101,14 +1124,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

-		case 50: {

+		case 51: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				Ident(out id);

 				label = id.val; 

-			} else if (la.kind == 18 || la.kind == 50) {

-				while (la.kind == 50) {

+			} else if (la.kind == 18 || la.kind == 51) {

+				while (la.kind == 51) {

 					Get();

 					breakCount++; 

 				}

@@ -1118,11 +1141,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

-		case 51: {

+		case 52: {

 			ReturnStmt(out s);

 			break;

 		}

-		case 27: {

+		case 30: {

 			Get();

 			s = new SkeletonStatement(t); 

 			Expect(18);

@@ -1134,16 +1157,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AssertStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-		Expression/*!*/ e = null; Attributes attrs = null;

+		Expression e = null; Attributes attrs = null;

 		

-		Expect(66);

-		x = t; s = null;

+		Expect(67);

+		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

 		if (StartOf(9)) {

 			Expression(out e);

-		} else if (la.kind == 27) {

+		} else if (la.kind == 30) {

 			Get();

 		} else SynErr(144);

 		Expect(18);

@@ -1156,19 +1179,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AssumeStmt(out Statement/*!*/ s) {

-		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 

-		Expect(54);

+		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+		Expression e = null; Attributes attrs = null;

+		

+		Expect(55);

 		x = t; 

-		Expression(out e);

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

+		if (StartOf(9)) {

+			Expression(out e);

+		} else if (la.kind == 30) {

+			Get();

+		} else SynErr(145);

+		if (e == null) {

+		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+		} else {

+		 s = new AssumeStmt(x, e, attrs);

+		}

+		

 		Expect(18);

-		s = new AssumeStmt(x, e); 

 	}

 

 	void PrintStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

 		

-		Expect(67);

+		Expect(68);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1199,14 +1236,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(18);

 			rhss.Add(new ExprRhs(e, attrs)); 

-		} else if (la.kind == 20 || la.kind == 52 || la.kind == 53) {

+		} else if (la.kind == 20 || la.kind == 53 || la.kind == 54) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 20) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 52) {

+			if (la.kind == 53) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

@@ -1216,20 +1253,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Rhs(out r, lhs0);

 					rhss.Add(r); 

 				}

-			} else if (la.kind == 53) {

+			} else if (la.kind == 54) {

 				Get();

 				x = t; 

-				if (la.kind == 54) {

+				if (la.kind == 55) {

 					Get();

 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(145);

+			} else SynErr(146);

 			Expect(18);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(146);

+		} else SynErr(147);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

@@ -1260,8 +1297,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 52 || la.kind == 53) {

-			if (la.kind == 52) {

+		if (la.kind == 53 || la.kind == 54) {

+			if (la.kind == 53) {

 				Get();

 				assignTok = t;

 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

@@ -1277,7 +1314,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				Get();

 				assignTok = t; 

-				if (la.kind == 54) {

+				if (la.kind == 55) {

 					Get();

 					suchThatAssume = t; 

 				}

@@ -1316,25 +1353,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(59);

+		Expect(60);

 		x = t; 

-		if (la.kind == 27 || la.kind == 33) {

-			if (la.kind == 33) {

+		if (la.kind == 22 || la.kind == 30) {

+			if (la.kind == 22) {

 				Guard(out guard);

 			} else {

 				Get();

 				guardOmitted = true; 

 			}

 			BlockStmt(out thn, out bodyStart, out bodyEnd);

-			if (la.kind == 60) {

+			if (la.kind == 61) {

 				Get();

-				if (la.kind == 59) {

+				if (la.kind == 60) {

 					IfStmt(out s);

 					els = s; 

 				} else if (la.kind == 6) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(147);

+				} else SynErr(148);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1345,7 +1382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(148);

+		} else SynErr(149);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1361,10 +1398,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(63);

+		Expect(64);

 		x = t; 

-		if (la.kind == 27 || la.kind == 33) {

-			if (la.kind == 33) {

+		if (la.kind == 22 || la.kind == 30) {

+			if (la.kind == 22) {

 				Guard(out guard);

 				Contract.Assume(guard == null || cce.Owner.None(guard)); 

 			} else {

@@ -1374,10 +1411,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			if (la.kind == 6) {

 				BlockStmt(out body, out bodyStart, out bodyEnd);

-			} else if (la.kind == 27) {

+			} else if (la.kind == 30) {

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(149);

+			} else SynErr(150);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

@@ -1395,18 +1432,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(150);

+		} else SynErr(151);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

-		Expect(65);

+		Expect(66);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1426,9 +1463,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(68);

+		Expect(69);

 		x = t; 

-		Expect(33);

+		Expect(22);

 		if (la.kind == 1) {

 			List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; 

 			QuantifierDomain(out bvarsX, out attrsX, out rangeX);

@@ -1438,14 +1475,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (bvars == null) { bvars = new List<BoundVar>(); }

 		if (range == null) { range = new LiteralExpr(x, true); }

 		

-		Expect(34);

-		while (la.kind == 29 || la.kind == 31) {

+		Expect(24);

+		while (la.kind == 32 || la.kind == 34) {

 			isFree = false; 

-			if (la.kind == 29) {

+			if (la.kind == 32) {

 				Get();

 				isFree = true; 

 			}

-			Expect(31);

+			Expect(34);

 			Expression(out e);

 			Expect(18);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

@@ -1459,7 +1496,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

 		

-		Expect(51);

+		Expect(52);

 		returnTok = t; 

 		if (StartOf(14)) {

 			Rhs(out r, null);

@@ -1483,27 +1520,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 55) {

+		if (la.kind == 56) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 33 || la.kind == 43 || la.kind == 56) {

-				if (la.kind == 56) {

+			if (la.kind == 22 || la.kind == 44 || la.kind == 57) {

+				if (la.kind == 57) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(57);

+					Expect(58);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

-				} else if (la.kind == 43) {

+				} else if (la.kind == 44) {

 					Get();

 					Ident(out x);

-					Expect(33);

+					Expect(22);

 					args = new List<Expression/*!*/>(); 

 					if (StartOf(9)) {

 						Expressions(args);

 					}

-					Expect(34);

+					Expect(24);

 					initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); 

 				} else {

 					Get();

@@ -1521,7 +1558,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					if (StartOf(9)) {

 						Expressions(args);

 					}

-					Expect(34);

+					Expect(24);

 					if (x != null) {

 					 initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

 					}

@@ -1534,18 +1571,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

-		} else if (la.kind == 58) {

+		} else if (la.kind == 59) {

 			Get();

 			x = t; 

 			Expression(out e);

 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 

-		} else if (la.kind == 47) {

+		} else if (la.kind == 48) {

 			Get();

 			r = new HavocRhs(t); 

 		} else if (StartOf(9)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(151);

+		} else SynErr(152);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1557,16 +1594,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 43 || la.kind == 56) {

+			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(15)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 43 || la.kind == 56) {

+			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

-		} else SynErr(152);

+		} else SynErr(153);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1582,15 +1619,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

-		Expect(33);

-		if (la.kind == 47) {

+		Expect(22);

+		if (la.kind == 48) {

 			Get();

 			e = null; 

 		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(153);

-		Expect(34);

+		} else SynErr(154);

+		Expect(24);

 	}

 

 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {

@@ -1600,11 +1637,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(62);

+			Expect(63);

 			body = new List<Statement>(); 

 			while (StartOf(10)) {

 				Stmt(body);

@@ -1622,22 +1659,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;

 		

 		while (StartOf(16)) {

-			if (la.kind == 29 || la.kind == 64) {

+			if (la.kind == 32 || la.kind == 65) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();}

 				Expect(18);

 				invariants.Add(invariant); 

-			} else if (la.kind == 32) {

-				while (!(la.kind == 0 || la.kind == 32)) {SynErr(155); Get();}

+			} else if (la.kind == 35) {

+				while (!(la.kind == 0 || la.kind == 35)) {SynErr(156); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();}

 				Expect(18);

 			} else {

-				while (!(la.kind == 0 || la.kind == 28)) {SynErr(157); Get();}

+				while (!(la.kind == 0 || la.kind == 31)) {SynErr(158); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1652,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();}

+				while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();}

 				Expect(18);

 			}

 		}

@@ -1660,12 +1697,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}

-		if (la.kind == 29) {

+		while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(160); Get();}

+		if (la.kind == 32) {

 			Get();

 			isFree = true; 

 		}

-		Expect(64);

+		Expect(65);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1680,10 +1717,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 22) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -1692,9 +1729,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(34);

+			Expect(24);

 		}

-		Expect(62);

+		Expect(63);

 		while (StartOf(10)) {

 			Stmt(body);

 		}

@@ -1709,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(160);

+		} else SynErr(161);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1737,7 +1774,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpression(out e0);

-		while (la.kind == 69 || la.kind == 70) {

+		while (la.kind == 70 || la.kind == 71) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1748,7 +1785,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0);

-		if (la.kind == 71 || la.kind == 72) {

+		if (la.kind == 72 || la.kind == 73) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1757,23 +1794,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 69) {

+		if (la.kind == 70) {

 			Get();

-		} else if (la.kind == 70) {

+		} else if (la.kind == 71) {

 			Get();

-		} else SynErr(161);

+		} else SynErr(162);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

 		if (StartOf(17)) {

-			if (la.kind == 73 || la.kind == 74) {

+			if (la.kind == 74 || la.kind == 75) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 73 || la.kind == 74) {

+				while (la.kind == 74 || la.kind == 75) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1784,7 +1821,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 75 || la.kind == 76) {

+				while (la.kind == 76 || la.kind == 77) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1795,11 +1832,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 71) {

+		if (la.kind == 72) {

 			Get();

-		} else if (la.kind == 72) {

+		} else if (la.kind == 73) {

 			Get();

-		} else SynErr(162);

+		} else SynErr(163);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

@@ -1893,19 +1930,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 73) {

+		if (la.kind == 74) {

 			Get();

-		} else if (la.kind == 74) {

+		} else if (la.kind == 75) {

 			Get();

-		} else SynErr(163);

+		} else SynErr(164);

 	}

 

 	void OrOp() {

-		if (la.kind == 75) {

+		if (la.kind == 76) {

 			Get();

-		} else if (la.kind == 76) {

+		} else if (la.kind == 77) {

 			Get();

-		} else SynErr(164);

+		} else SynErr(165);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -1924,17 +1961,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken y;

 		

 		switch (la.kind) {

-		case 77: {

+		case 23: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

-		case 22: {

+		case 25: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 23: {

+		case 26: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

@@ -1997,14 +2034,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(165); break;

+		default: SynErr(166); break;

 		}

 	}

 

 	void Factor(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 47 || la.kind == 89 || la.kind == 90) {

+		while (la.kind == 48 || la.kind == 89 || la.kind == 90) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2019,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 88) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(166);

+		} else SynErr(167);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

@@ -2039,43 +2076,43 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {

+		case 19: case 39: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 43 || la.kind == 56) {

+			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 56: {

+		case 6: case 57: {

 			DisplayExpr(out e);

 			break;

 		}

-		case 39: {

+		case 40: {

 			MultiSetExpr(out e);

 			break;

 		}

-		case 41: {

+		case 42: {

 			MapExpr(out e);

 			break;

 		}

-		case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			ConstAtomExpression(out e);

-			while (la.kind == 43 || la.kind == 56) {

+			while (la.kind == 44 || la.kind == 57) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(167); break;

+		default: SynErr(168); break;

 		}

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

 		} else if (la.kind == 89) {

@@ -2084,7 +2121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 90) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(168);

+		} else SynErr(169);

 	}

 

 	void NegOp() {

@@ -2092,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 91) {

 			Get();

-		} else SynErr(169);

+		} else SynErr(170);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2103,18 +2140,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 59: {

+		case 60: {

 			Get();

 			x = t; 

 			Expression(out e);

 			Expect(99);

 			Expression(out e0);

-			Expect(60);

+			Expect(61);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

-		case 65: {

+		case 66: {

 			MatchExpression(out e);

 			break;

 		}

@@ -2122,11 +2159,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			QuantifierGuts(out e);

 			break;

 		}

-		case 38: {

+		case 39: {

 			ComprehensionExpr(out e);

 			break;

 		}

-		case 66: {

+		case 67: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2135,7 +2172,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 54: {

+		case 55: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2156,7 +2193,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out d);

 				letVars.Add(d); 

 			}

-			Expect(52);

+			Expect(53);

 			Expression(out e);

 			letRHSs.Add(e); 

 			while (la.kind == 20) {

@@ -2169,7 +2206,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(170); break;

+		default: SynErr(171); break;

 		}

 	}

 

@@ -2180,18 +2217,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Ident(out id);

 		idents.Add(id); 

-		while (la.kind == 43) {

+		while (la.kind == 44) {

 			Get();

 			Ident(out id);

 			idents.Add(id); 

 		}

-		if (la.kind == 33) {

+		if (la.kind == 22) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

 			if (StartOf(9)) {

 				Expressions(args);

 			}

-			Expect(34);

+			Expect(24);

 		}

 		e = new IdentifierSequence(idents, openParen, args); 

 	}

@@ -2202,20 +2239,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Expression> multipleIndices = null;

 		bool func = false;

 		

-		if (la.kind == 43) {

+		if (la.kind == 44) {

 			Get();

 			Ident(out id);

-			if (la.kind == 33) {

+			if (la.kind == 22) {

 				Get();

 				IToken openParen = t;  args = new List<Expression/*!*/>();  func = true; 

 				if (StartOf(9)) {

 					Expressions(args);

 				}

-				Expect(34);

+				Expect(24);

 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

 			if (!func) { e = new ExprDotName(id, e, id.val); } 

-		} else if (la.kind == 56) {

+		} else if (la.kind == 57) {

 			Get();

 			x = t; 

 			if (StartOf(9)) {

@@ -2228,11 +2265,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						Expression(out ee);

 						e1 = ee; 

 					}

-				} else if (la.kind == 52) {

+				} else if (la.kind == 53) {

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 20 || la.kind == 57) {

+				} else if (la.kind == 20 || la.kind == 58) {

 					while (la.kind == 20) {

 						Get();

 						Expression(out ee);

@@ -2243,7 +2280,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(171);

+				} else SynErr(172);

 			} else if (la.kind == 100) {

 				Get();

 				anyDots = true; 

@@ -2251,7 +2288,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(172);

+			} else SynErr(173);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2274,8 +2311,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(57);

-		} else SynErr(173);

+			Expect(58);

+		} else SynErr(174);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2291,15 +2328,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 56) {

+		} else if (la.kind == 57) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(9)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(57);

-		} else SynErr(174);

+			Expect(58);

+		} else SynErr(175);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2307,7 +2344,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(39);

+		Expect(40);

 		x = t; 

 		if (la.kind == 6) {

 			Get();

@@ -2317,15 +2354,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new MultiSetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 33) {

+		} else if (la.kind == 22) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

-			Expect(34);

+			Expect(24);

 		} else if (StartOf(19)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(175);

+		} else SynErr(176);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2334,16 +2371,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<ExpressionPair/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(41);

+		Expect(42);

 		x = t; 

-		if (la.kind == 56) {

+		if (la.kind == 57) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(9)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(57);

+			Expect(58);

 		} else if (la.kind == 1) {

 			BoundVar/*!*/ bv;

 			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

@@ -2359,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(19)) {

 			SemErr("map must be followed by literal in brackets or comprehension."); 

-		} else SynErr(176);

+		} else SynErr(177);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -2396,27 +2433,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 96: {

 			Get();

 			x = t; 

-			Expect(33);

+			Expect(22);

 			Expression(out e);

-			Expect(34);

+			Expect(24);

 			e = new FreshExpr(x, e); 

 			break;

 		}

 		case 97: {

 			Get();

 			x = t; 

-			Expect(33);

+			Expect(22);

 			Expression(out e);

-			Expect(34);

+			Expect(24);

 			e = new AllocatedExpr(x, e); 

 			break;

 		}

 		case 98: {

 			Get();

 			x = t; 

-			Expect(33);

+			Expect(22);

 			Expression(out e);

-			Expect(34);

+			Expect(24);

 			e = new OldExpr(x, e); 

 			break;

 		}

@@ -2428,15 +2465,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(17);

 			break;

 		}

-		case 33: {

+		case 22: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new ParensExpression(x, e); 

-			Expect(34);

+			Expect(24);

 			break;

 		}

-		default: SynErr(177); break;

+		default: SynErr(178); break;

 		}

 	}

 

@@ -2455,13 +2492,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

 		Expression(out d);

-		Expect(52);

+		Expect(53);

 		Expression(out r);

 		elements.Add(new ExpressionPair(d,r)); 

 		while (la.kind == 20) {

 			Get();

 			Expression(out d);

-			Expect(52);

+			Expect(53);

 			Expression(out r);

 			elements.Add(new ExpressionPair(d,r)); 

 		}

@@ -2472,17 +2509,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 106) {

 			Get();

-		} else SynErr(178);

+		} else SynErr(179);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		

-		Expect(65);

+		Expect(66);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2503,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 103 || la.kind == 104) {

 			Exists();

 			x = t; 

-		} else SynErr(179);

+		} else SynErr(180);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2523,7 +2560,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(38);

+		Expect(39);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

@@ -2549,10 +2586,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 33) {

+		if (la.kind == 22) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -2561,9 +2598,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(34);

+			Expect(24);

 		}

-		Expect(62);

+		Expect(63);

 		Expression(out body);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

@@ -2573,7 +2610,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 102) {

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void Exists() {

@@ -2581,7 +2618,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(181);

+		} else SynErr(182);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2617,27 +2654,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, x,T,x,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

 

 	};

 } // end Parser

@@ -2684,62 +2721,62 @@ public class Errors {
 			case 19: s = "\"var\" expected"; break;

 			case 20: s = "\",\" expected"; break;

 			case 21: s = "\"type\" expected"; break;

-			case 22: s = "\"<\" expected"; break;

-			case 23: s = "\">\" expected"; break;

-			case 24: s = "\"method\" expected"; break;

-			case 25: s = "\"constructor\" expected"; break;

-			case 26: s = "\"returns\" expected"; break;

-			case 27: s = "\"...\" expected"; break;

-			case 28: s = "\"modifies\" expected"; break;

-			case 29: s = "\"free\" expected"; break;

-			case 30: s = "\"requires\" expected"; break;

-			case 31: s = "\"ensures\" expected"; break;

-			case 32: s = "\"decreases\" expected"; break;

-			case 33: s = "\"(\" expected"; break;

-			case 34: s = "\")\" expected"; break;

-			case 35: s = "\"bool\" expected"; break;

-			case 36: s = "\"nat\" expected"; break;

-			case 37: s = "\"int\" expected"; break;

-			case 38: s = "\"set\" expected"; break;

-			case 39: s = "\"multiset\" expected"; break;

-			case 40: s = "\"seq\" expected"; break;

-			case 41: s = "\"map\" expected"; break;

-			case 42: s = "\"object\" expected"; break;

-			case 43: s = "\".\" expected"; break;

-			case 44: s = "\"function\" expected"; break;

-			case 45: s = "\"predicate\" expected"; break;

-			case 46: s = "\"reads\" expected"; break;

-			case 47: s = "\"*\" expected"; break;

-			case 48: s = "\"`\" expected"; break;

-			case 49: s = "\"label\" expected"; break;

-			case 50: s = "\"break\" expected"; break;

-			case 51: s = "\"return\" expected"; break;

-			case 52: s = "\":=\" expected"; break;

-			case 53: s = "\":|\" expected"; break;

-			case 54: s = "\"assume\" expected"; break;

-			case 55: s = "\"new\" expected"; break;

-			case 56: s = "\"[\" expected"; break;

-			case 57: s = "\"]\" expected"; break;

-			case 58: s = "\"choose\" expected"; break;

-			case 59: s = "\"if\" expected"; break;

-			case 60: s = "\"else\" expected"; break;

-			case 61: s = "\"case\" expected"; break;

-			case 62: s = "\"=>\" expected"; break;

-			case 63: s = "\"while\" expected"; break;

-			case 64: s = "\"invariant\" expected"; break;

-			case 65: s = "\"match\" expected"; break;

-			case 66: s = "\"assert\" expected"; break;

-			case 67: s = "\"print\" expected"; break;

-			case 68: s = "\"parallel\" expected"; break;

-			case 69: s = "\"<==>\" expected"; break;

-			case 70: s = "\"\\u21d4\" expected"; break;

-			case 71: s = "\"==>\" expected"; break;

-			case 72: s = "\"\\u21d2\" expected"; break;

-			case 73: s = "\"&&\" expected"; break;

-			case 74: s = "\"\\u2227\" expected"; break;

-			case 75: s = "\"||\" expected"; break;

-			case 76: s = "\"\\u2228\" expected"; break;

-			case 77: s = "\"==\" expected"; break;

+			case 22: s = "\"(\" expected"; break;

+			case 23: s = "\"==\" expected"; break;

+			case 24: s = "\")\" expected"; break;

+			case 25: s = "\"<\" expected"; break;

+			case 26: s = "\">\" expected"; break;

+			case 27: s = "\"method\" expected"; break;

+			case 28: s = "\"constructor\" expected"; break;

+			case 29: s = "\"returns\" expected"; break;

+			case 30: s = "\"...\" expected"; break;

+			case 31: s = "\"modifies\" expected"; break;

+			case 32: s = "\"free\" expected"; break;

+			case 33: s = "\"requires\" expected"; break;

+			case 34: s = "\"ensures\" expected"; break;

+			case 35: s = "\"decreases\" expected"; break;

+			case 36: s = "\"bool\" expected"; break;

+			case 37: s = "\"nat\" expected"; break;

+			case 38: s = "\"int\" expected"; break;

+			case 39: s = "\"set\" expected"; break;

+			case 40: s = "\"multiset\" expected"; break;

+			case 41: s = "\"seq\" expected"; break;

+			case 42: s = "\"map\" expected"; break;

+			case 43: s = "\"object\" expected"; break;

+			case 44: s = "\".\" expected"; break;

+			case 45: s = "\"function\" expected"; break;

+			case 46: s = "\"predicate\" expected"; break;

+			case 47: s = "\"reads\" expected"; break;

+			case 48: s = "\"*\" expected"; break;

+			case 49: s = "\"`\" expected"; break;

+			case 50: s = "\"label\" expected"; break;

+			case 51: s = "\"break\" expected"; break;

+			case 52: s = "\"return\" expected"; break;

+			case 53: s = "\":=\" expected"; break;

+			case 54: s = "\":|\" expected"; break;

+			case 55: s = "\"assume\" expected"; break;

+			case 56: s = "\"new\" expected"; break;

+			case 57: s = "\"[\" expected"; break;

+			case 58: s = "\"]\" expected"; break;

+			case 59: s = "\"choose\" expected"; break;

+			case 60: s = "\"if\" expected"; break;

+			case 61: s = "\"else\" expected"; break;

+			case 62: s = "\"case\" expected"; break;

+			case 63: s = "\"=>\" expected"; break;

+			case 64: s = "\"while\" expected"; break;

+			case 65: s = "\"invariant\" expected"; break;

+			case 66: s = "\"match\" expected"; break;

+			case 67: s = "\"assert\" expected"; break;

+			case 68: s = "\"print\" expected"; break;

+			case 69: s = "\"parallel\" expected"; break;

+			case 70: s = "\"<==>\" expected"; break;

+			case 71: s = "\"\\u21d4\" expected"; break;

+			case 72: s = "\"==>\" expected"; break;

+			case 73: s = "\"\\u21d2\" expected"; break;

+			case 74: s = "\"&&\" expected"; break;

+			case 75: s = "\"\\u2227\" expected"; break;

+			case 76: s = "\"||\" expected"; break;

+			case 77: s = "\"\\u2228\" expected"; break;

 			case 78: s = "\"<=\" expected"; break;

 			case 79: s = "\">=\" expected"; break;

 			case 80: s = "\"!=\" expected"; break;

@@ -2807,43 +2844,44 @@ public class Errors {
 			case 142: s = "this symbol not expected in OneStmt"; break;

 			case 143: s = "invalid OneStmt"; break;

 			case 144: s = "invalid AssertStmt"; break;

-			case 145: s = "invalid UpdateStmt"; break;

+			case 145: s = "invalid AssumeStmt"; break;

 			case 146: s = "invalid UpdateStmt"; break;

-			case 147: s = "invalid IfStmt"; break;

+			case 147: s = "invalid UpdateStmt"; break;

 			case 148: s = "invalid IfStmt"; break;

-			case 149: s = "invalid WhileStmt"; break;

+			case 149: s = "invalid IfStmt"; break;

 			case 150: s = "invalid WhileStmt"; break;

-			case 151: s = "invalid Rhs"; break;

-			case 152: s = "invalid Lhs"; break;

-			case 153: s = "invalid Guard"; break;

-			case 154: s = "this symbol not expected in LoopSpec"; break;

+			case 151: s = "invalid WhileStmt"; break;

+			case 152: s = "invalid Rhs"; break;

+			case 153: s = "invalid Lhs"; break;

+			case 154: s = "invalid Guard"; break;

 			case 155: s = "this symbol not expected in LoopSpec"; break;

 			case 156: s = "this symbol not expected in LoopSpec"; break;

 			case 157: s = "this symbol not expected in LoopSpec"; break;

 			case 158: s = "this symbol not expected in LoopSpec"; break;

-			case 159: s = "this symbol not expected in Invariant"; break;

-			case 160: s = "invalid AttributeArg"; break;

-			case 161: s = "invalid EquivOp"; break;

-			case 162: s = "invalid ImpliesOp"; break;

-			case 163: s = "invalid AndOp"; break;

-			case 164: s = "invalid OrOp"; break;

-			case 165: s = "invalid RelOp"; break;

-			case 166: s = "invalid AddOp"; break;

-			case 167: s = "invalid UnaryExpression"; break;

-			case 168: s = "invalid MulOp"; break;

-			case 169: s = "invalid NegOp"; break;

-			case 170: s = "invalid EndlessExpression"; break;

-			case 171: s = "invalid Suffix"; break;

+			case 159: s = "this symbol not expected in LoopSpec"; break;

+			case 160: s = "this symbol not expected in Invariant"; break;

+			case 161: s = "invalid AttributeArg"; break;

+			case 162: s = "invalid EquivOp"; break;

+			case 163: s = "invalid ImpliesOp"; break;

+			case 164: s = "invalid AndOp"; break;

+			case 165: s = "invalid OrOp"; break;

+			case 166: s = "invalid RelOp"; break;

+			case 167: s = "invalid AddOp"; break;

+			case 168: s = "invalid UnaryExpression"; break;

+			case 169: s = "invalid MulOp"; break;

+			case 170: s = "invalid NegOp"; break;

+			case 171: s = "invalid EndlessExpression"; break;

 			case 172: s = "invalid Suffix"; break;

 			case 173: s = "invalid Suffix"; break;

-			case 174: s = "invalid DisplayExpr"; break;

-			case 175: s = "invalid MultiSetExpr"; break;

-			case 176: s = "invalid MapExpr"; break;

-			case 177: s = "invalid ConstAtomExpression"; break;

-			case 178: s = "invalid QSep"; break;

-			case 179: s = "invalid QuantifierGuts"; break;

-			case 180: s = "invalid Forall"; break;

-			case 181: s = "invalid Exists"; break;

+			case 174: s = "invalid Suffix"; break;

+			case 175: s = "invalid DisplayExpr"; break;

+			case 176: s = "invalid MultiSetExpr"; break;

+			case 177: s = "invalid MapExpr"; break;

+			case 178: s = "invalid ConstAtomExpression"; break;

+			case 179: s = "invalid QSep"; break;

+			case 180: s = "invalid QuantifierGuts"; break;

+			case 181: s = "invalid Forall"; break;

+			case 182: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index fb46ba4b..3654c672 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -71,6 +71,9 @@ namespace Microsoft.Dafny {
           if (i++ != 0) { wr.WriteLine(); }

           Indent(indent);

           PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

+          if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {

+            wr.Write("(==)");

+          }

           wr.WriteLine(";");

         } else if (d is DatatypeDecl) {

           if (i++ != 0) { wr.WriteLine(); }

@@ -149,6 +152,9 @@ namespace Microsoft.Dafny {
         foreach (TypeParameter tp in typeArgs) {

           Contract.Assert(tp != null);

           wr.Write("{0}{1}", sep, tp.Name);

+          if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {

+            wr.Write("(==)");

+          }

           sep = ", ";

         }

         wr.Write(">");

@@ -427,24 +433,14 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (stmt is AssertStmt) {

-        Expression expr = ((AssertStmt)stmt).Expr;

-

-        wr.Write("assert");

-

-        if (stmt.HasAttributes())

-        {

+      if (stmt is PredicateStmt) {

+        Expression expr = ((PredicateStmt)stmt).Expr;

+        wr.Write(stmt is AssertStmt ? "assert" : "assume");

+        if (stmt.HasAttributes()) {

           PrintAttributes(stmt.Attributes);

         }

-

         wr.Write(" ");

         PrintExpression(expr);

-

-        wr.Write(";");

-

-      } else if (stmt is AssumeStmt) {

-        wr.Write("assume ");

-        PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

 

       } else if (stmt is PrintStmt) {

@@ -629,6 +625,9 @@ namespace Microsoft.Dafny {
         } else if (s.S is AssertStmt) {

           Contract.Assert(s.ConditionOmitted);

           wr.Write("assert ...;");

+        } else if (s.S is AssumeStmt) {

+          Contract.Assert(s.ConditionOmitted);

+          wr.Write("assume ...;");

         } else if (s.S is IfStmt) {

           PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);

         } else if (s.S is WhileStmt) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 56006a7f..bbc12d6a 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class RefinementTransformer

+  public class RefinementTransformer : IRewriter

   {

     ResolutionErrorReporter reporter;

     public RefinementTransformer(ResolutionErrorReporter reporter) {

@@ -59,12 +59,17 @@ namespace Microsoft.Dafny {
     }

 

     private ModuleDecl moduleUnderConstruction;  // non-null for the duration of Construct calls

+    private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

 

-    public void Construct(ModuleDecl m) {

-      Contract.Requires(m != null);

-      Contract.Requires(m.RefinementBase != null);

+    public void PreResolve(ModuleDecl m) {

+      if (m.RefinementBase == null) {

+        // This Rewriter doesn't do anything

+        return;

+      }

 

-      Contract.Assert(moduleUnderConstruction == null);

+      if (moduleUnderConstruction != null) {

+        postTasks.Clear();

+      }

       moduleUnderConstruction = m;

       var prev = m.RefinementBase;

 

@@ -99,7 +104,35 @@ namespace Microsoft.Dafny {
         } else {

           var nw = m.TopLevelDecls[index];

           if (d is ArbitraryTypeDecl) {

-            // this is allowed to be refined by any type declaration, so just keep the new one

+            bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;

+            if (nw is ArbitraryTypeDecl) {

+              if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {

+                reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);

+              }

+            } else if (dDemandsEqualitySupport) {

+              if (nw is ClassDecl) {

+                // fine, as long as "nw" does not take any type parameters

+                if (nw.TypeArgs.Count != 0) {

+                  reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);

+                }

+              } else if (nw is CoDatatypeDecl) {

+                reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

+              } else {

+                Contract.Assert(nw is IndDatatypeDecl);

+                if (nw.TypeArgs.Count != 0) {

+                  reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);

+                } else {

+                  // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

+                  // taken place, so we defer it until the PostResolve phase.

+                  var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());

+                  postTasks.Enqueue(delegate() {

+                    if (!udt.SupportsEquality) {

+                      reporter.Error(udt.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);

+                    }

+                  });

+                }

+              }

+            }

           } else if (nw is ArbitraryTypeDecl) {

             reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

           } else if (nw is DatatypeDecl) {

@@ -115,7 +148,18 @@ namespace Microsoft.Dafny {
         }

       }

 

-      Contract.Assert(moduleUnderConstruction == m);

+      Contract.Assert(moduleUnderConstruction == m);  // this should be as it was set earlier in this method

+    }

+

+    public void PostResolve(ModuleDecl m) {

+      if (m == moduleUnderConstruction) {

+        while (this.postTasks.Count != 0) {

+          var a = postTasks.Dequeue();

+          a();

+        }

+      } else {

+        postTasks.Clear();

+      }

       moduleUnderConstruction = null;

     }

 

@@ -135,7 +179,7 @@ namespace Microsoft.Dafny {
 

       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

-        return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);

+        return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

@@ -165,7 +209,7 @@ namespace Microsoft.Dafny {
     }

 

     TypeParameter CloneTypeParam(TypeParameter tp) {

-      return new TypeParameter(Tok(tp.tok), tp.Name);

+      return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);

     }

 

     MemberDecl CloneMember(MemberDecl member) {

@@ -429,11 +473,11 @@ namespace Microsoft.Dafny {
       Statement r;

       if (stmt is AssertStmt) {

         var s = (AssertStmt)stmt;

-        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is AssumeStmt) {

         var s = (AssumeStmt)stmt;

-        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is PrintStmt) {

         var s = (PrintStmt)stmt;

@@ -598,6 +642,8 @@ namespace Microsoft.Dafny {
     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

+      CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "class");

+

       // Create a simple name-to-member dictionary.  Ignore any duplicates at this time.

       var declaredNames = new Dictionary<string, int>();

       for (int i = 0; i < nw.Members.Count; i++) {

@@ -731,6 +777,27 @@ namespace Microsoft.Dafny {
           var n = nw[i];

           if (o.Name != n.Name) {

             reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);

+          } else {

+            // This explains what we want to do and why:

+            // switch (o.EqualitySupport) {

+            //   case TypeParameter.EqualitySupportValue.Required:

+            //     // here, we will insist that the new type-parameter also explicitly requires equality support (because we don't want

+            //     // to wait for the inference to run on the new module)

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Required;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.InferredRequired:

+            //     // here, we can allow anything, because even with an Unspecified value, the inference will come up with InferredRequired, like before

+            //     good = true;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.Unspecified:

+            //     // inference didn't come up with anything on the previous module, so the only value we'll allow here is Unspecified as well

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified;

+            //     break;

+            // }

+            // Here's how we actually compute it:

+            if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport) {

+              reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);

+            }

           }

         }

       }

@@ -794,6 +861,8 @@ namespace Microsoft.Dafny {
            *   assert ...;                 assert E;                    assert E;

            *   assert E;                                                assert E;

            *   

+           *   assume ...;                 assume E;                    assume E;

+           *   

            *   var x := E;                 var x;                       var x := E;

            *   var x := E;                 var x := *;                  var x := E;

            *   var x := E1;                var x :| E0;                 var x := E1; assert E0;

@@ -855,6 +924,19 @@ namespace Microsoft.Dafny {
                 i++; j++;

               }

 

+            } else if (S is AssumeStmt) {

+              var skel = (AssumeStmt)S;

+              Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

+              var oldAssume = oldS as AssumeStmt;

+              if (oldAssume == null) {

+                reporter.Error(cur.Tok, "assume template does not match inherited statement");

+                i++;

+              } else {

+                var e = CloneExpr(oldAssume.Expr);

+                body.Add(new AssumeStmt(skel.Tok, e, null));

+                i++; j++;

+              }

+

             } else if (S is IfStmt) {

               var skel = (IfStmt)S;

               Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

@@ -928,7 +1010,7 @@ namespace Microsoft.Dafny {
               body.Add(cNew);

               i++; j++;

               if (addedAssert != null) {

-                body.Add(new AssertStmt(addedAssert.tok, addedAssert));

+                body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));

               }

             } else {

               MergeAddStatement(cur, body);

@@ -1006,6 +1088,8 @@ namespace Microsoft.Dafny {
         var S = ((SkeletonStatement)nxt).S;

         if (S is AssertStmt) {

           return other is PredicateStmt;

+        } else if (S is AssumeStmt) {

+          return other is AssumeStmt;

         } else if (S is IfStmt) {

           return other is IfStmt;

         } else if (S is WhileStmt) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index f0990aa0..3d99f732 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -170,15 +170,17 @@ namespace Microsoft.Dafny {
       }

 

       // register top-level declarations

-      Rewriter rewriter = new AutoContractsRewriter();

+      var rewriters = new List<IRewriter>();

+      // The following line could be generalized to allow rewriter plug-ins; to support such, just add command-line

+      // switches and .Add to "rewriters" here.

+      rewriters.Add(new AutoContractsRewriter());

+      rewriters.Add(new RefinementTransformer(this));

+

       var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);

       var moduleNameInfo = new ModuleNameInformation[h];

       foreach (var m in mm) {

-        rewriter.PreResolve(m);

-        if (m.RefinementBase != null) {

-          var transformer = new RefinementTransformer(this);

-          transformer.Construct(m);

-        }

+        rewriters.Iter(r => r.PreResolve(m));

+

         moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);

 

         // set up environment

@@ -187,13 +189,16 @@ namespace Microsoft.Dafny {
         allDatatypeCtors = info.Ctors;

         // resolve

         var datatypeDependencies = new Graph<IndDatatypeDecl>();

+        int prevErrorCount = ErrorCount;

         ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

-        ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+        if (prevErrorCount == ErrorCount) {

+          ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+        }

         // tear down

         classes = null;

         allDatatypeCtors = null;

-        // give rewriter a chance to do processing

-        rewriter.PostResolve(m);

+        // give rewriters a chance to do processing

+        rewriters.Iter(r => r.PostResolve(m));

       }

 

       // compute IsRecursive bit for mutually recursive functions

@@ -394,15 +399,16 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

 

-      // Perform the stratosphere check on inductive datatypes

+      // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support

       foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {

         if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {

           // do the following check once per SCC, so call it on each SCC representative

           SccStratosphereCheck(dtd, datatypeDependencies);

+          DetermineEqualitySupport(dtd, datatypeDependencies);

         }

       }

-      // Perform the guardedness check on co-datatypes

       if (ErrorCount == prevErrorCount) {  // because CheckCoCalls requires the given expression to have been successfully resolved

+        // Perform the guardedness check on co-datatypes

         foreach (var decl in declarations) {

           var cl = decl as ClassDecl;

           if (cl != null) {

@@ -426,7 +432,396 @@ namespace Microsoft.Dafny {
             }

           }

         }

+        // Inferred required equality support for datatypes and for Function and Method signatures

+        // First, do datatypes until a fixpoint is reached

+        bool inferredSomething;

+        do {

+          inferredSomething = false;

+          foreach (var d in declarations) {

+            if (d is DatatypeDecl) {

+              var dt = (DatatypeDecl)d;

+              foreach (var tp in dt.TypeArgs) {

+                if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                  // here's our chance to infer the need for equality support

+                  foreach (var ctor in dt.Ctors) {

+                    foreach (var arg in ctor.Formals) {

+                      if (InferRequiredEqualitySupport(tp, arg.Type)) {

+                        tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                        inferredSomething = true;

+                        goto DONE_DT;  // break out of the doubly-nested loop

+                      }

+                    }

+                  }

+                DONE_DT: ;

+                }

+              }

+            }

+          }

+        } while (inferredSomething);

+        // Now do it for Function and Method signatures

+        foreach (var d in declarations) {

+          if (d is ClassDecl) {

+            var cl = (ClassDecl)d;

+            foreach (var member in cl.Members) {

+              if (!member.IsGhost) {

+                if (member is Function) {

+                  var f = (Function)member;

+                  foreach (var tp in f.TypeArgs) {

+                    if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                      // here's our chance to infer the need for equality support

+                      if (InferRequiredEqualitySupport(tp, f.ResultType)) {

+                        tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                      } else {

+                        foreach (var p in f.Formals) {

+                          if (InferRequiredEqualitySupport(tp, p.Type)) {

+                            tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                            break;

+                          }

+                        }

+                      }

+                    }

+                  }

+                } else if (member is Method) {

+                  var m = (Method)member;

+                  foreach (var tp in m.TypeArgs) {

+                    if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                      // here's our chance to infer the need for equality support

+                      foreach (var p in m.Ins) {

+                        if (InferRequiredEqualitySupport(tp, p.Type)) {

+                          tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                          goto DONE;

+                        }

+                      }

+                      foreach (var p in m.Outs) {

+                        if (InferRequiredEqualitySupport(tp, p.Type)) {

+                          tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                          goto DONE;

+                        }

+                      }

+                    DONE: ;

+                    }

+                  }

+                }

+              }

+            }

+          }

+        }

+        // Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.

+        // Note that this check can only be done after determining which expressions are ghosts.

+        foreach (var d in declarations) {

+          if (d is ClassDecl) {

+            var cl = (ClassDecl)d;

+            foreach (var member in cl.Members) {

+              if (!member.IsGhost) {

+                if (member is Field) {

+                  var f = (Field)member;

+                  CheckEqualityTypes_Type(f.tok, f.Type);

+                } else if (member is Function) {

+                  var f = (Function)member;

+                  foreach (var p in f.Formals) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  CheckEqualityTypes_Type(f.tok, f.ResultType);

+                  if (f.Body != null) {

+                    CheckEqualityTypes(f.Body);

+                  }

+                } else if (member is Method) {

+                  var m = (Method)member;

+                  foreach (var p in m.Ins) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  foreach (var p in m.Outs) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  if (m.Body != null) {

+                    CheckEqualityTypes_Stmt(m.Body);

+                  }

+                }

+              }

+            }

+          } else if (d is DatatypeDecl) {

+            var dt = (DatatypeDecl)d;

+            foreach (var ctor in dt.Ctors) {

+              foreach (var p in ctor.Formals) {

+                if (!p.IsGhost) {

+                  CheckEqualityTypes_Type(p.tok, p.Type);

+                }

+              }

+            }

+          }

+        }

+      }

+    }

+

+    void CheckEqualityTypes_Stmt(Statement stmt) {

+      Contract.Requires(stmt != null);

+      if (stmt.IsGhost) {

+        return;

+      } else if (stmt is PrintStmt) {

+        var s = (PrintStmt)stmt;

+        foreach (var arg in s.Args) {

+          if (arg.E != null) {

+            CheckEqualityTypes(arg.E);

+          }

+        }

+      } else if (stmt is BreakStmt) {

+      } else if (stmt is ReturnStmt) {

+        var s = (ReturnStmt)stmt;

+        if (s.rhss != null) {

+          s.rhss.Iter(CheckEqualityTypes_Rhs);

+        }

+      } else if (stmt is AssignStmt) {

+        AssignStmt s = (AssignStmt)stmt;

+        CheckEqualityTypes(s.Lhs);

+        CheckEqualityTypes_Rhs(s.Rhs);

+      } else if (stmt is VarDecl) {

+        var s = (VarDecl)stmt;

+        s.SubStatements.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is CallStmt) {

+        var s = (CallStmt)stmt;

+        CheckEqualityTypes(s.Receiver);

+        s.Args.Iter(CheckEqualityTypes);

+        s.Lhs.Iter(CheckEqualityTypes);

+

+        Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);

+        var i = 0;

+        foreach (var formalTypeArg in s.Method.TypeArgs) {

+          var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];

+          if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {

+            Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));

+          }

+          i++;

+        }

+      } else if (stmt is BlockStmt) {

+        var s = (BlockStmt)stmt;

+        s.Body.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is IfStmt) {

+        var s = (IfStmt)stmt;

+        if (s.Guard != null) {

+          CheckEqualityTypes(s.Guard);

+        }

+        s.SubStatements.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is AlternativeStmt) {

+        var s = (AlternativeStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          CheckEqualityTypes(alt.Guard);

+          alt.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is WhileStmt) {

+        var s = (WhileStmt)stmt;

+        if (s.Guard != null) {

+          CheckEqualityTypes(s.Guard);

+        }

+        CheckEqualityTypes_Stmt(s.Body);

+      } else if (stmt is AlternativeLoopStmt) {

+        var s = (AlternativeLoopStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          CheckEqualityTypes(alt.Guard);

+          alt.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

+        CheckEqualityTypes(s.Range);

+        CheckEqualityTypes_Stmt(s.Body);

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

+        CheckEqualityTypes(s.Source);

+        foreach (MatchCaseStmt mc in s.Cases) {

+          mc.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is ConcreteSyntaxStatement) {

+        var s = (ConcreteSyntaxStatement)stmt;

+        s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

+      }

+    }

+

+    void CheckEqualityTypes_Rhs(AssignmentRhs rhs) {

+      Contract.Requires(rhs != null);

+      rhs.SubExpressions.Iter(CheckEqualityTypes);

+      rhs.SubStatements.Iter(CheckEqualityTypes_Stmt);

+    }

+

+    void CheckEqualityTypes(Expression expr) {

+      Contract.Requires(expr != null);

+      if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        var t0 = e.E0.Type.Normalize();

+        var t1 = e.E1.Type.Normalize();

+        switch (e.Op) {

+          case BinaryExpr.Opcode.Eq:

+          case BinaryExpr.Opcode.Neq:

+            // First, check a special case:  a datatype value (like Nil) that takes no parameters

+            var e0 = e.E0.Resolved as DatatypeValue;

+            var e1 = e.E1.Resolved as DatatypeValue;

+            if (e0 != null && e0.Arguments.Count == 0) {

+              // that's cool

+            } else if (e1 != null && e1.Arguments.Count == 0) {

+              // oh yeah!

+            } else if (!t0.SupportsEquality) {

+              Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+            } else if (!t1.SupportsEquality) {

+              Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));

+            }

+            break;

+          default:

+            switch (e.ResolvedOp) {

+              // Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how

+              // these types are instantiated.  (Except: This guarantee does not apply to equality on maps, because the Range type

+              // of maps is not restricted, only the Domain type.  However, the equality operator is checked above.)

+              case BinaryExpr.ResolvedOpcode.InSeq:

+              case BinaryExpr.ResolvedOpcode.NotInSeq:

+              case BinaryExpr.ResolvedOpcode.Prefix:

+              case BinaryExpr.ResolvedOpcode.ProperPrefix:

+                if (!t1.SupportsEquality) {

+                  Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));

+                } else if (!t0.SupportsEquality) {

+                  if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {

+                    Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+                  } else {

+                    Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+                  }

+                }

+                break;

+              default:

+                break;

+            }

+            break;

+        }

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

+        foreach (var bv in e.BoundVars) {

+          CheckEqualityTypes_Type(bv.tok, bv.Type);

+        }

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var bv in e.Vars) {

+          CheckEqualityTypes_Type(bv.tok, bv.Type);

+        }

+      } else if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);

+        var i = 0;

+        foreach (var formalTypeArg in e.Function.TypeArgs) {

+          var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];

+          if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {

+            Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));

+          }

+          i++;

+        }

+      }

+

+      foreach (var ee in expr.SubExpressions) {

+        CheckEqualityTypes(ee);

+      }

+    }

+

+    void CheckEqualityTypes_Type(IToken tok, Type type) {

+      Contract.Requires(tok != null);

+      Contract.Requires(type != null);

+      type = type.Normalize();

+      if (type is BasicType) {

+        // fine

+      } else if (type is SetType) {

+        var argType = ((SetType)type).Arg;

+        if (!argType.SupportsEquality) {

+          Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));

+        }

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is MultiSetType) {

+        var argType = ((MultiSetType)type).Arg;

+        if (!argType.SupportsEquality) {

+          Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));

+        }

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is MapType) {

+        var mt = (MapType)type;

+        if (!mt.Domain.SupportsEquality) {

+          Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));

+        }

+        CheckEqualityTypes_Type(tok, mt.Domain);

+        CheckEqualityTypes_Type(tok, mt.Range);

+

+      } else if (type is SeqType) {

+        Type argType = ((SeqType)type).Arg;

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is UserDefinedType) {

+        var udt = (UserDefinedType)type;

+        if (udt.ResolvedClass != null) {

+          Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);

+          var i = 0;

+          foreach (var argType in udt.TypeArgs) {

+            var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+            if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {

+              Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));

+            }

+            CheckEqualityTypes_Type(tok, argType);

+            i++;

+          }

+        } else {

+          Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

+        }

+

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

+      }

+    }

+

+    string TypeEqualityErrorMessageHint(Type argType) {

+      Contract.Requires(argType != null);

+      var tp = argType.AsTypeParameter;

+      if (tp != null) {

+        return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line);

+      }

+      return "";

+    }

+

+    bool InferRequiredEqualitySupport(TypeParameter tp, Type type) {

+      Contract.Requires(tp != null);

+      Contract.Requires(type != null);

+

+      type = type.Normalize();

+      if (type is BasicType) {

+      } else  if (type is SetType) {

+        var st = (SetType)type;

+        return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);

+      } else if (type is MultiSetType) {

+        var ms = (MultiSetType)type;

+        return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg);

+      } else if (type is MapType) {

+        var mt = (MapType)type;

+        return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range);

+      } else if (type is SeqType) {

+        var sq = (SeqType)type;

+        return InferRequiredEqualitySupport(tp, sq.Arg);

+      } else if (type is UserDefinedType) {

+        var udt = (UserDefinedType)type;

+        if (udt.ResolvedClass != null) {

+          var i = 0;

+          foreach (var argType in udt.TypeArgs) {

+            var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+            if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {

+              return true;

+            }

+            i++;

+          }

+        } else {

+          Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

+        }

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

+      return false;

     }

 

     ClassDecl currentClass;

@@ -655,6 +1050,99 @@ namespace Microsoft.Dafny {
       return true;

     }

 

+    void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {

+      Contract.Requires(startingPoint != null);

+      Contract.Requires(dependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));

+

+      var scc = dependencies.GetSCC(startingPoint);

+      // First, the simple case:  If any parameter of any inductive datatype in the SCC is of a codatatype type, then

+      // the whole SCC is incapable of providing the equality operation.

+      foreach (var dt in scc) {

+        Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);

+        foreach (var ctor in dt.Ctors) {

+          foreach (var arg in ctor.Formals) {

+            var anotherIndDt = arg.Type.AsIndDatatype;

+            if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {

+              // arg.Type is known never to support equality

+              // So, go around the entire SCC and record what we learnt

+              foreach (var ddtt in scc) {

+                ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;

+              }

+              return;  // we are done

+            }

+          }

+        }

+      }

+

+      // Now for the more involved case:  we need to determine which type parameters determine equality support for each datatype in the SCC

+      // We start by seeing where each datatype's type parameters are used in a place known to determine equality support.

+      bool thingsChanged = false;

+      foreach (var dt in scc) {

+        if (dt.TypeArgs.Count == 0) {

+          // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors

+          continue;

+        }

+        foreach (var ctor in dt.Ctors) {

+          foreach (var arg in ctor.Formals) {

+            var typeArg = arg.Type.AsTypeParameter;

+            if (typeArg != null) {

+              typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+              thingsChanged = true;

+            } else {

+              var otherDt = arg.Type.AsIndDatatype;

+              if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) {  // datatype is in a different SCC

+                var otherUdt = (UserDefinedType)arg.Type.Normalize();

+                var i = 0;

+                foreach (var otherTp in otherDt.TypeArgs) {

+                  if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                    var tp = otherUdt.TypeArgs[i].AsTypeParameter;

+                    if (tp != null) {

+                      tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+                      thingsChanged = true;

+                    }

+                  }

+                }

+              }

+            }

+          }

+        }

+      }

+      // Then we propagate this information up through the SCC

+      while (thingsChanged) {

+        thingsChanged = false;

+        foreach (var dt in scc) {

+          if (dt.TypeArgs.Count == 0) {

+            // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors

+            continue;

+          }

+          foreach (var ctor in dt.Ctors) {

+            foreach (var arg in ctor.Formals) {

+              var otherDt = arg.Type.AsIndDatatype;

+              if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC

+                var otherUdt = (UserDefinedType)arg.Type.Normalize();

+                var i = 0;

+                foreach (var otherTp in otherDt.TypeArgs) {

+                  if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                    var tp = otherUdt.TypeArgs[i].AsTypeParameter;

+                    if (tp != null && !tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                      tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+                      thingsChanged = true;

+                    }

+                  }

+                  i++;

+                }

+              }

+            }

+          }

+        }

+      }

+      // Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones

+      // where equality support should be checked by looking at the type arguments.

+      foreach (var dt in scc) {

+        dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;

+      }

+    }

+

     void ResolveAttributes(Attributes attrs, bool twoState) {

       // order does not matter much for resolution, so resolve them in reverse order

       for (; attrs != null; attrs = attrs.Prev) {

@@ -1133,7 +1621,7 @@ namespace Microsoft.Dafny {
 

       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy

       } else if (proxy is DatatypeProxy) {

-        if (t.IsDatatype) {

+        if (t.IsIndDatatype) {

           // all is fine, proxy can be redirected to t

         } else {

           return false;

@@ -1146,14 +1634,6 @@ namespace Microsoft.Dafny {
           return false;

         }

 

-      } else if (proxy is ObjectsTypeProxy) {

-        if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

-          // all is good

-        } else if (t is CollectionType) {

-          proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());

-          return UnifyTypes(proxy.T, t);

-        }

-

       } else if (proxy is CollectionTypeProxy) {

         CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;

         if (t is CollectionType) {

@@ -1235,10 +1715,6 @@ namespace Microsoft.Dafny {
           // all is fine

           a.T = b;

           return true;

-        } else if (b is ObjectsTypeProxy) {

-          // unify a and b by redirecting b to a, since a gives the stronger requirement

-          b.T = a;

-          return true;

         } else if (b is IndexableTypeProxy) {

           // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type

           a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);

@@ -1248,37 +1724,6 @@ namespace Microsoft.Dafny {
           return false;

         }

 

-      } else if (a is ObjectsTypeProxy) {

-        if (b is ObjectsTypeProxy) {

-          // fine

-          a.T = b;

-          return true;

-        } else if (b is CollectionTypeProxy) {

-          // fine provided b's collection-element-type can be unified with object or a class type

-          a.T = b;

-          return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());

-        } else if (b is OperationTypeProxy) {

-          // fine; restrict a to sets of object/class, and restrict b to set/seq of object/class

-          if (((OperationTypeProxy)b).AllowSeq) {

-            a.T = new CollectionTypeProxy(new ObjectTypeProxy());

-            b.T = a.T;

-          } else {

-            a.T = new SetType(new ObjectTypeProxy());

-            b.T = a.T;

-          }

-          return true;

-        } else if (b is IndexableTypeProxy) {

-          IndexableTypeProxy pb = (IndexableTypeProxy)b;

-          // the intersection of ObjectsTypeProxy and IndexableTypeProxy is

-          // EITHER a sequence of ObjectTypeProxy OR an array of anything OR map of ObjectTypeProxy in either domain or range.

-          // TODO: here, only the first of the three cases is supported

-          b.T = new SeqType(pb.Arg);

-          a.T = b.T;

-          return UnifyTypes(pb.Arg, new ObjectTypeProxy());

-        } else {

-          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected restricted-proxy type

-        }

-

       } else if (a is CollectionTypeProxy) {

         if (b is CollectionTypeProxy) {

           a.T = b;

@@ -2122,22 +2567,22 @@ namespace Microsoft.Dafny {
         UserDefinedType ctype = (UserDefinedType)nptype;  // TODO: get rid of this statement, make this code handle any non-proxy type

 #endif

         // build the type substitution map

-        Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

+        s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

         for (int i = 0; i < ctype.TypeArgs.Count; i++) {

-          subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

+          s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

         }

         foreach (TypeParameter p in callee.TypeArgs) {

-          subst.Add(p, new ParamTypeProxy(p));

+          s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));

         }

         // type check the arguments

         for (int i = 0; i < callee.Ins.Count; i++) {

-          Type st = SubstType(callee.Ins[i].Type, subst);

+          Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);

           if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {

             Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);

           }

         }

         for (int i = 0; i < callee.Outs.Count; i++) {

-          Type st = SubstType(callee.Outs[i].Type, subst);

+          Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);

           var lhs = s.Lhs[i];

           if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {

             Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

@@ -2925,12 +3370,12 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

             {

-              if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsDatatype) {

+              if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

                 expr.Type = Type.Bool;

-              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {

+              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);

                 }

@@ -2959,7 +3404,7 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Gt:

           case BinaryExpr.Opcode.Ge:

             {

-              if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsDatatype) {

+              if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

@@ -3467,24 +3912,24 @@ namespace Microsoft.Dafny {
             }

           }

           // build the type substitution map

-          Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

+          e.TypeArgumentSubstitutions =  new Dictionary<TypeParameter, Type>();

           for (int i = 0; i < ctype.TypeArgs.Count; i++) {

-            subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

+            e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

           }

           foreach (TypeParameter p in function.TypeArgs) {

-            subst.Add(p, new ParamTypeProxy(p));

+            e.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));

           }

           // type check the arguments

           for (int i = 0; i < function.Formals.Count; i++) {

             Expression farg = e.Args[i];

             ResolveExpression(farg, twoState);

             Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression

-            Type s = SubstType(function.Formals[i].Type, subst);

+            Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);

             if (!UnifyTypes(farg.Type, s)) {

               Error(e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);

             }

           }

-          e.Type = SubstType(function.ResultType, subst);

+          e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);

         }

 

         // Resolution termination check

@@ -4112,6 +4557,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(e.Seq.Type != null);  // follows from postcondition of ResolveExpression

       Type elementType = new InferredTypeProxy();

       Type domainType = new InferredTypeProxy();

+      

       IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);

       if (!UnifyTypes(e.Seq.Type, expectedType)) {

         Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);

@@ -4197,7 +4643,7 @@ namespace Microsoft.Dafny {
             return BinaryExpr.ResolvedOpcode.Disjoint;

           }

         case BinaryExpr.Opcode.Lt:

-          if (operandType.IsDatatype || operandType is DatatypeProxy) {

+          if (operandType.IsIndDatatype || operandType is DatatypeProxy) {

             return BinaryExpr.ResolvedOpcode.RankLt;

           } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSubset;

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 26ec496e..e04c5e9b 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -4,11 +4,22 @@ using System.Diagnostics.Contracts;
 

 namespace Microsoft.Dafny

 {

-  public interface Rewriter

+  [ContractClass(typeof(IRewriterContracts))]

+  public interface IRewriter

   {

     void PreResolve(ModuleDecl m);

     void PostResolve(ModuleDecl m);

   }

+  [ContractClassFor(typeof(IRewriter))]

+  abstract class IRewriterContracts : IRewriter

+  {

+    public void PreResolve(ModuleDecl m) {

+      Contract.Requires(m != null);

+    }

+    public void PostResolve(ModuleDecl m) {

+      Contract.Requires(m != null);

+    }

+  }

 

   /// <summary>

   /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate

@@ -48,7 +59,7 @@ namespace Microsoft.Dafny
   ///    if (A != null) { Repr := Repr + {A}; }

   ///    if (F != null) { Repr := Repr + {F} + F.Repr; }

   /// </summary>

-  public class AutoContractsRewriter : Rewriter

+  public class AutoContractsRewriter : IRewriter

   {

     public void PreResolve(ModuleDecl m) {

       foreach (var d in m.TopLevelDecls) {

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index d35fc22f..7cb302fa 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -265,11 +265,11 @@ public class Scanner {
 		start[124] = 58; 

 		start[59] = 19; 

 		start[44] = 20; 

+		start[40] = 21; 

+		start[41] = 22; 

 		start[60] = 59; 

 		start[62] = 60; 

 		start[46] = 61; 

-		start[40] = 22; 

-		start[41] = 23; 

 		start[42] = 24; 

 		start[96] = 25; 

 		start[91] = 28; 

@@ -498,40 +498,40 @@ public class Scanner {
 			case "codatatype": t.kind = 15; break;

 			case "var": t.kind = 19; break;

 			case "type": t.kind = 21; break;

-			case "method": t.kind = 24; break;

-			case "constructor": t.kind = 25; break;

-			case "returns": t.kind = 26; break;

-			case "modifies": t.kind = 28; break;

-			case "free": t.kind = 29; break;

-			case "requires": t.kind = 30; break;

-			case "ensures": t.kind = 31; break;

-			case "decreases": t.kind = 32; break;

-			case "bool": t.kind = 35; break;

-			case "nat": t.kind = 36; break;

-			case "int": t.kind = 37; break;

-			case "set": t.kind = 38; break;

-			case "multiset": t.kind = 39; break;

-			case "seq": t.kind = 40; break;

-			case "map": t.kind = 41; break;

-			case "object": t.kind = 42; break;

-			case "function": t.kind = 44; break;

-			case "predicate": t.kind = 45; break;

-			case "reads": t.kind = 46; break;

-			case "label": t.kind = 49; break;

-			case "break": t.kind = 50; break;

-			case "return": t.kind = 51; break;

-			case "assume": t.kind = 54; break;

-			case "new": t.kind = 55; break;

-			case "choose": t.kind = 58; break;

-			case "if": t.kind = 59; break;

-			case "else": t.kind = 60; break;

-			case "case": t.kind = 61; break;

-			case "while": t.kind = 63; break;

-			case "invariant": t.kind = 64; break;

-			case "match": t.kind = 65; break;

-			case "assert": t.kind = 66; break;

-			case "print": t.kind = 67; break;

-			case "parallel": t.kind = 68; break;

+			case "method": t.kind = 27; break;

+			case "constructor": t.kind = 28; break;

+			case "returns": t.kind = 29; break;

+			case "modifies": t.kind = 31; break;

+			case "free": t.kind = 32; break;

+			case "requires": t.kind = 33; break;

+			case "ensures": t.kind = 34; break;

+			case "decreases": t.kind = 35; break;

+			case "bool": t.kind = 36; break;

+			case "nat": t.kind = 37; break;

+			case "int": t.kind = 38; break;

+			case "set": t.kind = 39; break;

+			case "multiset": t.kind = 40; break;

+			case "seq": t.kind = 41; break;

+			case "map": t.kind = 42; break;

+			case "object": t.kind = 43; break;

+			case "function": t.kind = 45; break;

+			case "predicate": t.kind = 46; break;

+			case "reads": t.kind = 47; break;

+			case "label": t.kind = 50; break;

+			case "break": t.kind = 51; break;

+			case "return": t.kind = 52; break;

+			case "assume": t.kind = 55; break;

+			case "new": t.kind = 56; break;

+			case "choose": t.kind = 59; break;

+			case "if": t.kind = 60; break;

+			case "else": t.kind = 61; break;

+			case "case": t.kind = 62; break;

+			case "while": t.kind = 64; break;

+			case "invariant": t.kind = 65; break;

+			case "match": t.kind = 66; break;

+			case "assert": t.kind = 67; break;

+			case "print": t.kind = 68; break;

+			case "parallel": t.kind = 69; break;

 			case "in": t.kind = 82; break;

 			case "false": t.kind = 92; break;

 			case "true": t.kind = 93; break;

@@ -652,47 +652,47 @@ public class Scanner {
 			case 20:

 				{t.kind = 20; break;}

 			case 21:

-				{t.kind = 27; break;}

+				{t.kind = 22; break;}

 			case 22:

-				{t.kind = 33; break;}

+				{t.kind = 24; break;}

 			case 23:

-				{t.kind = 34; break;}

+				{t.kind = 30; break;}

 			case 24:

-				{t.kind = 47; break;}

-			case 25:

 				{t.kind = 48; break;}

+			case 25:

+				{t.kind = 49; break;}

 			case 26:

-				{t.kind = 52; break;}

-			case 27:

 				{t.kind = 53; break;}

+			case 27:

+				{t.kind = 54; break;}

 			case 28:

-				{t.kind = 56; break;}

-			case 29:

 				{t.kind = 57; break;}

+			case 29:

+				{t.kind = 58; break;}

 			case 30:

-				{t.kind = 62; break;}

+				{t.kind = 63; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 69; break;}

-			case 33:

 				{t.kind = 70; break;}

-			case 34:

+			case 33:

 				{t.kind = 71; break;}

-			case 35:

+			case 34:

 				{t.kind = 72; break;}

+			case 35:

+				{t.kind = 73; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 73; break;}

-			case 38:

 				{t.kind = 74; break;}

-			case 39:

+			case 38:

 				{t.kind = 75; break;}

-			case 40:

+			case 39:

 				{t.kind = 76; break;}

+			case 40:

+				{t.kind = 77; break;}

 			case 41:

 				{t.kind = 79; break;}

 			case 42:

@@ -731,41 +731,41 @@ public class Scanner {
 				else {t.kind = 5; break;}

 			case 57:

 				recEnd = pos; recKind = 16;

-				if (ch == '>') {AddCh(); goto case 30;}

-				else if (ch == '=') {AddCh(); goto case 63;}

+				if (ch == '=') {AddCh(); goto case 63;}

+				else if (ch == '>') {AddCh(); goto case 30;}

 				else {t.kind = 16; break;}

 			case 58:

 				recEnd = pos; recKind = 17;

 				if (ch == '|') {AddCh(); goto case 39;}

 				else {t.kind = 17; break;}

 			case 59:

-				recEnd = pos; recKind = 22;

+				recEnd = pos; recKind = 25;

 				if (ch == '=') {AddCh(); goto case 64;}

-				else {t.kind = 22; break;}

+				else {t.kind = 25; break;}

 			case 60:

-				recEnd = pos; recKind = 23;

+				recEnd = pos; recKind = 26;

 				if (ch == '=') {AddCh(); goto case 41;}

-				else {t.kind = 23; break;}

+				else {t.kind = 26; break;}

 			case 61:

-				recEnd = pos; recKind = 43;

+				recEnd = pos; recKind = 44;

 				if (ch == '.') {AddCh(); goto case 65;}

-				else {t.kind = 43; break;}

+				else {t.kind = 44; break;}

 			case 62:

 				recEnd = pos; recKind = 83;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

 				else {t.kind = 83; break;}

 			case 63:

-				recEnd = pos; recKind = 77;

+				recEnd = pos; recKind = 23;

 				if (ch == '>') {AddCh(); goto case 34;}

-				else {t.kind = 77; break;}

+				else {t.kind = 23; break;}

 			case 64:

 				recEnd = pos; recKind = 78;

 				if (ch == '=') {AddCh(); goto case 31;}

 				else {t.kind = 78; break;}

 			case 65:

 				recEnd = pos; recKind = 100;

-				if (ch == '.') {AddCh(); goto case 21;}

+				if (ch == '.') {AddCh(); goto case 23;}

 				else {t.kind = 100; break;}

 

 		}

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index cb880767..ddc51368 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -259,10 +259,10 @@ namespace GPUVerify
 

         private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)

         {

-            Expr CTimesLocalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr, 

+            Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr, 

                 new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

 

-            Expr CTimesLocalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

                 new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

 

             Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));

@@ -293,10 +293,10 @@ namespace GPUVerify
 

         private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)

         {

-            Expr CTimesGlobalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,

                 GlobalIdExpr("X", Thread));

 

-            Expr CTimesGlobalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,

+            Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

                 GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

 

             Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 40e27310..e3d94fcc 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -61,8 +61,6 @@ namespace GPUVerify
         public IRaceInstrumenter RaceInstrumenter;

 

         public UniformityAnalyser uniformityAnalyser;

-        public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;

-        public MayBeGidAnalyser mayBeGidAnalyser;

         public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;

         public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;

         public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;

@@ -361,7 +359,7 @@ namespace GPUVerify
 

             DoUniformityAnalysis();

 

-            DoMayBeTidAnalysis();

+            DoVariableDefinitionAnalysis();

 

             DoMayBeIdPlusConstantAnalysis();

 

@@ -369,8 +367,6 @@ namespace GPUVerify
 

             DoArrayControlFlowAnalysis();

 

-            DoVariableDefinitionAnalysis();

-

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_preprocessed");

@@ -483,15 +479,6 @@ namespace GPUVerify
             mayBePowerOfTwoAnalyser.Analyse();

         }

 

-        private void DoMayBeTidAnalysis()

-        {

-            mayBeTidAnalyser = new MayBeThreadConfigurationVariableAnalyser(this);

-            mayBeTidAnalyser.Analyse();

-

-            mayBeGidAnalyser = new MayBeGidAnalyser(this);

-            mayBeGidAnalyser.Analyse();

-        }

-

         private void DoMayBeIdPlusConstantAnalysis()

         {

             mayBeTidPlusConstantAnalyser = new MayBeLocalIdPlusConstantAnalyser(this);

@@ -1040,15 +1027,29 @@ namespace GPUVerify
             return _GROUP_SIZE_Z != null;

         }

 

-        internal static string StripThreadIdentifier(string p)

+        internal static string StripThreadIdentifier(string p, out int id)

         {

-            if (p.Contains("$"))

+            if (p.EndsWith("$1"))

+            {

+                id = 1;

+                return p.Substring(0, p.Length - 2);

+            }

+            if (p.EndsWith("$2"))

             {

-                return p.Substring(0, p.LastIndexOf("$"));

+                id = 2;

+                return p.Substring(0, p.Length - 2);

             }

+

+            id = 0;

             return p;

         }

 

+        internal static string StripThreadIdentifier(string p)

+        {

+            int id;

+            return StripThreadIdentifier(p, out id);

+        }

+

         private void AddStartAndEndBarriers()

         {

             CallCmd FirstBarrier = new CallCmd(KernelImplementation.tok, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

@@ -1299,7 +1300,9 @@ namespace GPUVerify
         private Expr MakeBVFunctionCall(string functionName, string smtName, Microsoft.Boogie.Type resultType, params Expr[] args)

         {

             Function f = GetOrCreateBVFunction(functionName, smtName, resultType, args.Select(a => a.Type).ToArray());

-            return new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));

+            var e = new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));

+            e.Type = resultType;

+            return e;

         }

 

         private Expr MakeBitVectorBinaryBoolean(string suffix, string smtName, Expr lhs, Expr rhs)

@@ -1316,6 +1319,12 @@ namespace GPUVerify
         internal Expr MakeBVSgt(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGT", "bvsgt", lhs, rhs); }

         internal Expr MakeBVSge(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGE", "bvsge", lhs, rhs); }

 

+        internal Expr MakeBVAnd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("AND", "bvand", lhs, rhs); }

+        internal Expr MakeBVAdd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("ADD", "bvadd", lhs, rhs); }

+        internal Expr MakeBVSub(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("SUB", "bvsub", lhs, rhs); }

+        internal Expr MakeBVMul(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("MUL", "bvmul", lhs, rhs); }

+        internal Expr MakeBVURem(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("UREM", "bvurem", lhs, rhs); }

+

         internal static Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)

         {

             return new NAryExpr(lhs.tok, new FunctionCall(new Function(lhs.tok, functionName, new VariableSeq(new Variable[] { 

@@ -1332,6 +1341,42 @@ namespace GPUVerify
             }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.GetBvType(32))))), new ExprSeq(new Expr[] { lhs, rhs }));

         }

 

+        private static bool IsBVFunctionCall(Expr e, string smtName, out ExprSeq args)

+        {

+            args = null;

+            var ne = e as NAryExpr;

+            if (ne == null)

+                return false;

+

+            var fc = ne.Fun as FunctionCall;

+            if (fc == null)

+                return false;

+

+            string bvBuiltin = QKeyValue.FindStringAttribute(fc.Func.Attributes, "bvbuiltin");

+            if (bvBuiltin == smtName)

+            {

+                args = ne.Args;

+                return true;

+            }

+

+            return false;

+        }

+

+        private static bool IsBVFunctionCall(Expr e, string smtName, out Expr lhs, out Expr rhs)

+        {

+            ExprSeq es;

+            if (IsBVFunctionCall(e, smtName, out es))

+            {

+                lhs = es[0]; rhs = es[1];

+                return true;

+            }

+            lhs = null; rhs = null;

+            return false;

+        }

+

+        internal static bool IsBVAdd(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvadd", out lhs, out rhs); }

+        internal static bool IsBVMul(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvmul", out lhs, out rhs); }

+

         internal Constant GetGroupSize(string dimension)

         {

             Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));

@@ -2291,14 +2336,9 @@ namespace GPUVerify
             return !arrayControlFlowAnalyser.MayAffectControlFlow(v.Name);

         }

 

-        internal static Expr StripThreadIdentifiers(Expr e)

-        {

-            return new ThreadIdentifierStripper().VisitExpr(e.Clone() as Expr);

-        }

-

         internal Expr GlobalIdExpr(string dimension)

         {

-            return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",

+            return MakeBVAdd(MakeBVMul(

                             new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))),

                                 new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension)));

         }

@@ -2310,14 +2350,112 @@ namespace GPUVerify
           else

               return new StructuredRegion(Impl);

         }

-    }

 

-    class ThreadIdentifierStripper : StandardVisitor

-    {

-        public override Variable VisitVariable(Variable node)

+

+        public static bool IsGivenConstant(Expr e, Constant c)

+        {

+            if (!(e is IdentifierExpr))

+                return false;

+

+            var varName = ((IdentifierExpr)e).Decl.Name;

+            return (StripThreadIdentifier(varName) == StripThreadIdentifier(c.Name));

+        }

+

+        public bool SubstIsGivenConstant(Implementation impl, Expr e, Constant c)

+        {

+            if (!(e is IdentifierExpr))

+                return false;

+            e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);

+            return IsGivenConstant(e, c);

+        }

+

+        public Constant GetLocalIdConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _X;

+                case 1:  return _Y;

+                case 2:  return _Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public Constant GetGroupIdConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _GROUP_X;

+                case 1:  return _GROUP_Y;

+                case 2:  return _GROUP_Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public Constant GetGroupSizeConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _GROUP_SIZE_X;

+                case 1:  return _GROUP_SIZE_Y;

+                case 2:  return _GROUP_SIZE_Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public bool IsLocalId(Expr e, int dim, Implementation impl)

+        {

+            return SubstIsGivenConstant(impl, e, GetLocalIdConst(dim));

+        }

+

+        public bool IsGlobalId(Expr e, int dim, Implementation impl)

+        {

+            e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);

+

+            if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))

+            {

+                NAryExpr nary = e as NAryExpr;

+                Constant localId = GetLocalIdConst(dim);

+

+                if (IsGivenConstant(nary.Args[1], localId))

+                {

+                    return IsGroupIdTimesGroupSize(nary.Args[0], dim);

+                }

+

+                if (IsGivenConstant(nary.Args[0], localId))

+                {

+                    return IsGroupIdTimesGroupSize(nary.Args[1], dim);

+                }

+            }

+

+            return false;

+        }

+

+        private bool IsGroupIdTimesGroupSize(Expr expr, int dim)

+        {

+            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))

+            {

+                NAryExpr innerNary = expr as NAryExpr;

+

+                if (IsGroupIdAndSize(dim, innerNary.Args[0], innerNary.Args[1]))

+                {

+                    return true;

+                }

+

+                if (IsGroupIdAndSize(dim, innerNary.Args[1], innerNary.Args[0]))

+                {

+                    return true;

+                }

+            }

+            return false;

+        }

+

+        private bool IsGroupIdAndSize(int dim, Expr maybeGroupId, Expr maybeGroupSize)

         {

-            node.Name = GPUVerifier.StripThreadIdentifier(node.Name);

-            return base.VisitVariable(node);

+            return IsGivenConstant(maybeGroupId, GetGroupIdConst(dim)) &&

+                   IsGivenConstant(maybeGroupSize, GetGroupSizeConst(dim));

         }

     }

 

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index eba91cd2..6762e634 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -113,13 +113,11 @@
     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

     <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />

     <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />

-    <Compile Include="MayBeGidAnalyser.cs" />

     <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />

     <Compile Include="KernelDualiser.cs" />

     <Compile Include="LiveVariableAnalyser.cs" />

     <Compile Include="LoopInvariantGenerator.cs" />

     <Compile Include="MayBePowerOfTwoAnalyser.cs" />

-    <Compile Include="MayBeThreadConfigurationVariableAnalyser.cs" />

     <Compile Include="MayBeIdPlusConstantAnalyser.cs" />

     <Compile Include="StructuredProgramVisitor.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs
deleted file mode 100644
index f7d8c973..00000000
--- a/Source/GPUVerify/MayBeGidAnalyser.cs
+++ /dev/null
@@ -1,320 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    class MayBeGidAnalyser : MayBeAnalyser

-    {

-        private static string[] dimensions = { "x", "y", "z" };

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

-        private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;

-

-        public MayBeGidAnalyser(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-

-            mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();

-            foreach (string s in dimensions)

-            {

-                mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();

-            }

-        

-        }

-

-        internal void Analyse()

-        {

-            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-            {

-                if(D is Implementation)

-                {

-                    Implementation Impl = D as Implementation;

-

-                    foreach (string s in dimensions)

-                    {

-                        mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();

-                    }

-

-                    foreach (Variable v in Impl.LocVars)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.InParams)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    ProcedureChanged = true;

-                }

-            }

-

-            while (ProcedureChanged)

-            {

-                ProcedureChanged = false;

-

-                foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-                {

-                    if (D is Implementation)

-                    {

-                        Implementation Impl = D as Implementation;

-                        Analyse(Impl);

-                    }

-                }

-            }

-

-            if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)

-            {

-                dump();

-            }

-        }

-

-        private void Analyse(Implementation Impl)

-        {

-            Analyse(Impl, verifier.RootRegion(Impl));

-        }

-

-        private void Analyse(Implementation impl, IRegion region)

-        {

-            foreach (Cmd c in region.Cmds())

-            {

-                if (c is AssignCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferAssign(impl, c as AssignCmd, s);

-                    }

-                }

-                else if (c is CallCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferCall(impl, c as CallCmd, s);

-                    }

-                }

-                else if (c is HavocCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferHavoc(impl, c as HavocCmd, s);

-                    }

-                }

-            }

-        }

-

-        private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)

-        {

-            Debug.Assert(havoc.Vars.Length == 1);

-            if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))

-            {

-                SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);

-            }

-        }

-

-        private void TransferCall(Implementation impl, CallCmd callCmd, string component)

-        {

-            if (callCmd.callee != verifier.BarrierProcedure.Name)

-            {

-

-                Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

-                for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

-                {

-                    if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)

-                        && !MayBe(component, impl.Name, callCmd.Ins[i]))

-                    {

-                        SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);

-                    }

-                }

-

-                for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)

-                {

-                    if (MayBe(component, impl.Name, callCmd.Outs[i].Name)

-                        && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))

-                    {

-                        SetNot(component, impl.Name, callCmd.Outs[i].Name);

-                    }

-                }

-

-            }

-        }

-

-        private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

-        {

-            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

-            {

-                if (assignCmd.Lhss[i] is SimpleAssignLhs)

-                {

-                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

-                    Expr rhs = assignCmd.Rhss[i];

-

-                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                        && !MayBe(component, impl.Name, rhs))

-                    {

-                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                    }

-                }

-            }

-        }

-

-        private void SetNot(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = false;

-            ProcedureChanged = true;

-        }

-

-        private void SetMayBe(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = true;

-        }

-

-        override internal bool MayBe(string component, string proc, string v)

-        {

-            if (!mayBeInfo[component].ContainsKey(proc))

-            {

-                return false;

-            }

-

-            if (!mayBeInfo[component][proc].ContainsKey(v))

-            {

-                return false;

-            }

-

-            return mayBeInfo[component][proc][v];

-        }

-

-        override internal bool MayBe(string component, string proc, Expr e)

-        {

-            if (e is IdentifierExpr)

-            {

-                return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);

-            }

-

-            if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))

-            {

-                NAryExpr nary = e as NAryExpr;

-

-                string localIdString = null;

-

-                if (component.Equals("x"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_X_STRING;

-                }

-                else if (component.Equals("y"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_Y_STRING;

-                }

-                else if (component.Equals("z"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_Z_STRING;

-                }

-                else

-                {

-                    Debug.Assert(false);

-                }

-

-                if(verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[1]))

-                {

-                    return IsGroupIdTimesGroupSize(component, proc, nary.Args[0]);

-                }

-

-                if (verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[0]))

-                {

-                    return IsGroupIdTimesGroupSize(component, proc, nary.Args[1]);

-                }

-            }

-

-            return false;

-        }

-

-        private bool IsGroupIdTimesGroupSize(string component, string proc, Expr expr)

-        {

-            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))

-            {

-                NAryExpr innerNary = expr as NAryExpr;

-

-                if (IsGroupIdAndSize(component, proc, innerNary.Args[0], innerNary.Args[1]))

-                {

-                    return true;

-                }

-

-                if (IsGroupIdAndSize(component, proc, innerNary.Args[1], innerNary.Args[0]))

-                {

-                    return true;

-                }

-            }

-            return false;

-        }

-

-        private bool IsGroupIdAndSize(string component, string proc, Expr maybeGroupId, Expr maybeGroupSize)

-        {

-            string groupIdString = null;

-            string groupSizeString = null;

-            if (component.Equals("x"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_X_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;

-            }

-            else if (component.Equals("y"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_Y_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;

-            }

-            else if (component.Equals("z"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_Z_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;

-            }

-            else

-            {

-                Debug.Assert(false);

-            }

-

-            return verifier.mayBeTidAnalyser.MayBe(groupIdString, proc, maybeGroupId) &&

-                                       verifier.mayBeTidAnalyser.MayBe(groupSizeString, proc, maybeGroupSize);

-        }

-

-        private void dump()

-        {

-            foreach (string s in dimensions)

-            {

-                Console.WriteLine("*** global_id_" + s + " ***");

-

-                foreach (string p in mayBeInfo[s].Keys)

-                {

-                    Console.WriteLine("  Procedure " + p);

-

-                    foreach (string v in mayBeInfo[s][p].Keys)

-                    {

-                        if (mayBeInfo[s][p][v])

-                        {

-                            Console.WriteLine("    " + v + ": may be global_id_" + s);

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
index a57f35ee..3ee8edc8 100644
--- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
+++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
@@ -11,8 +11,6 @@ namespace GPUVerify
     {

         protected GPUVerifier verifier;

 

-        protected MayBeAnalyser mayBeAnalyser;

-

         // Given a p.v, says whether p.v may be assigned to a tid variable at some point

         protected Dictionary<string, Dictionary<string, bool>> mayBeAssignedId;

 

@@ -104,7 +102,7 @@ namespace GPUVerify
 

                                     Variable rhsV = (assign.Rhss[i] as IdentifierExpr).Decl;

 

-                                    if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))

+                                    if (IsId(assign.Rhss[i], impl))

                                     {

                                         mayBeAssignedId[impl.Name][lhsV.Name] = true;

                                     }

@@ -128,6 +126,7 @@ namespace GPUVerify
             }

         }

 

+

         private string ConvertToString(Expr constantIncrement)

         {

             if (constantIncrement is IdentifierExpr)

@@ -217,7 +216,7 @@ namespace GPUVerify
 

         internal abstract string idKind();

 

-        protected abstract string ComponentString();

+        protected abstract bool IsId(Expr expr, Implementation impl);

 

         internal Expr GetIncrement(string p, string v)

         {

@@ -260,7 +259,11 @@ namespace GPUVerify
 

         internal MayBeLocalIdPlusConstantAnalyser(GPUVerifier verifier) : base(verifier)

         {

-            mayBeAnalyser = verifier.mayBeTidAnalyser;

+        }

+

+        protected override bool IsId(Expr expr, Implementation impl)

+        {

+            return verifier.IsLocalId(expr, 0, impl);

         }

 

         override internal Expr MakeIdExpr()

@@ -272,11 +275,6 @@ namespace GPUVerify
         {

             return "local id";

         }

-

-        protected override string ComponentString()

-        {

-            return GPUVerifier.LOCAL_ID_X_STRING;

-        }

     }

 

     class MayBeGlobalIdPlusConstantAnalyser : MayBeIdPlusConstantAnalyser

@@ -284,7 +282,11 @@ namespace GPUVerify
         internal MayBeGlobalIdPlusConstantAnalyser(GPUVerifier verifier)

             : base(verifier)

         {

-            mayBeAnalyser = verifier.mayBeGidAnalyser;

+        }

+

+        protected override bool IsId(Expr expr, Implementation impl)

+        {

+            return verifier.IsGlobalId(expr, 0, impl);

         }

 

         internal override string idKind()

@@ -296,12 +298,6 @@ namespace GPUVerify
         {

             return verifier.GlobalIdExpr("X");

         }

-

-        protected override string ComponentString()

-        {

-            return "x";

-        }

-

     }

 

 

diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
deleted file mode 100644
index d445d422..00000000
--- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
+++ /dev/null
@@ -1,273 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    abstract class MayBeAnalyser

-    {

-        abstract internal bool MayBe(string component, string proc, string v);

-        abstract internal bool MayBe(string component, string proc, Expr e);

-    }

-

-    class MayBeThreadConfigurationVariableAnalyser : MayBeAnalyser

-    {

-        private static string[] SpecialNames = { 

-            GPUVerifier.LOCAL_ID_X_STRING,

-            GPUVerifier.LOCAL_ID_Y_STRING,

-            GPUVerifier.LOCAL_ID_Z_STRING,

-            GPUVerifier.GROUP_ID_X_STRING,

-            GPUVerifier.GROUP_ID_Y_STRING,

-            GPUVerifier.GROUP_ID_Z_STRING,

-            GPUVerifier.NUM_GROUPS_X_STRING,

-            GPUVerifier.NUM_GROUPS_Y_STRING,

-            GPUVerifier.NUM_GROUPS_Z_STRING,

-            GPUVerifier.GROUP_SIZE_X_STRING,

-            GPUVerifier.GROUP_SIZE_Y_STRING,

-            GPUVerifier.GROUP_SIZE_Z_STRING

-        };

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

-        private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;

-

-        public MayBeThreadConfigurationVariableAnalyser(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-

-            mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();

-            foreach (string s in SpecialNames)

-            {

-                mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();

-            }

-        

-        }

-

-        internal void Analyse()

-        {

-            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-            {

-                if(D is Implementation)

-                {

-                    Implementation Impl = D as Implementation;

-

-                    foreach (string s in SpecialNames)

-                    {

-                        mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();

-                    }

-

-                    SetMayBe(GPUVerifier.LOCAL_ID_X_STRING, Impl.Name, GPUVerifier._X.Name);

-                    SetMayBe(GPUVerifier.LOCAL_ID_Y_STRING, Impl.Name, GPUVerifier._Y.Name);

-                    SetMayBe(GPUVerifier.LOCAL_ID_Z_STRING, Impl.Name, GPUVerifier._Z.Name);

-

-                    SetMayBe(GPUVerifier.GROUP_ID_X_STRING, Impl.Name, GPUVerifier._GROUP_X.Name);

-                    SetMayBe(GPUVerifier.GROUP_ID_Y_STRING, Impl.Name, GPUVerifier._GROUP_Y.Name);

-                    SetMayBe(GPUVerifier.GROUP_ID_Z_STRING, Impl.Name, GPUVerifier._GROUP_Z.Name);

-

-                    SetMayBe(GPUVerifier.GROUP_SIZE_X_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_X.Name);

-                    SetMayBe(GPUVerifier.GROUP_SIZE_Y_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Y.Name);

-                    SetMayBe(GPUVerifier.GROUP_SIZE_Z_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Z.Name);

-

-                    SetMayBe(GPUVerifier.NUM_GROUPS_X_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_X.Name);

-                    SetMayBe(GPUVerifier.NUM_GROUPS_Y_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Y.Name);

-                    SetMayBe(GPUVerifier.NUM_GROUPS_Z_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Z.Name);

-

-                    foreach (Variable v in Impl.LocVars)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.InParams)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    ProcedureChanged = true;

-                }

-            }

-

-            while (ProcedureChanged)

-            {

-                ProcedureChanged = false;

-

-                foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-                {

-                    if (D is Implementation)

-                    {

-                        Implementation Impl = D as Implementation;

-                        Analyse(Impl);

-                    }

-                }

-            }

-

-            if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)

-            {

-                dump();

-            }

-        }

-

-        private void Analyse(Implementation Impl)

-        {

-            Analyse(Impl, verifier.RootRegion(Impl));

-        }

-

-        private void Analyse(Implementation impl, IRegion region)

-        {

-            foreach (Cmd c in region.Cmds())

-            {

-                if (c is AssignCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferAssign(impl, c as AssignCmd, s);

-                    }

-                }

-                else if (c is CallCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferCall(impl, c as CallCmd, s);

-                    }

-                }

-                else if (c is HavocCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferHavoc(impl, c as HavocCmd, s);

-                    }

-                }

-            }

-        }

-

-        private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)

-        {

-            Debug.Assert(havoc.Vars.Length == 1);

-            if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))

-            {

-                SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);

-            }

-        }

-

-        private void TransferCall(Implementation impl, CallCmd callCmd, string component)

-        {

-            if (callCmd.callee != verifier.BarrierProcedure.Name)

-            {

-

-                Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

-                for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

-                {

-                    if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)

-                        && !MayBe(component, impl.Name, callCmd.Ins[i]))

-                    {

-                        SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);

-                    }

-                }

-

-                for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)

-                {

-                    if (MayBe(component, impl.Name, callCmd.Outs[i].Name)

-                        && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))

-                    {

-                        SetNot(component, impl.Name, callCmd.Outs[i].Name);

-                    }

-                }

-

-            }

-        }

-

-        private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

-        {

-            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

-            {

-                if (assignCmd.Lhss[i] is SimpleAssignLhs)

-                {

-                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

-                    Expr rhs = assignCmd.Rhss[i];

-

-                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                        && !MayBe(component, impl.Name, rhs))

-                    {

-                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                    }

-                }

-            }

-        }

-

-        private void SetNot(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = false;

-            ProcedureChanged = true;

-        }

-

-        private void SetMayBe(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = true;

-        }

-

-        override internal bool MayBe(string component, string proc, string v)

-        {

-            if (!mayBeInfo[component].ContainsKey(proc))

-            {

-                return false;

-            }

-

-            if (!mayBeInfo[component][proc].ContainsKey(v))

-            {

-                return false;

-            }

-

-            return mayBeInfo[component][proc][v];

-        }

-

-        override internal bool MayBe(string component, string proc, Expr e)

-        {

-            if (e is IdentifierExpr)

-            {

-                return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);

-            }

-            return false;

-        }

-

-        private void dump()

-        {

-            foreach (string s in SpecialNames)

-            {

-                Console.WriteLine("*** " + s + " ***");

-

-                foreach (string p in mayBeInfo[s].Keys)

-                {

-                    Console.WriteLine("  Procedure " + p);

-

-                    foreach (string v in mayBeInfo[s][p].Keys)

-                    {

-                        if (mayBeInfo[s][p][v])

-                        {

-                            Console.WriteLine("    " + v + ": may be " + s);

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 13a4585b..5a75fa21 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -131,121 +131,145 @@ namespace GPUVerify
             }

         }

 

-        private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

+        private class StrideConstraint {}

+        private class EqStrideConstraint : StrideConstraint {

+            public EqStrideConstraint(Expr eq) { this.eq = eq; }

+            public Expr eq;

+        }

+        private class ModStrideConstraint : StrideConstraint {

+            public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }

+            public Expr mod, modEq;

+        }

+

+        private StrideConstraint BuildBottomStrideConstraint(Expr e)

         {

-            if (!(e is NAryExpr))

-            {

-                return false;

-            }

+            int width = e.Type.BvBits;

+            return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),

+                                           new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));

+        }

 

-            NAryExpr nary = e as NAryExpr;

+        private bool IsBottomStrideConstraint(StrideConstraint sc)

+        {

+            var msc = sc as ModStrideConstraint;

+            if (msc == null)

+                return false;

 

-            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))

-            {

+            var le = msc.mod as LiteralExpr;

+            if (le == null)

                 return false;

-            }

 

-            {

-                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], true, impl);

-                if (constant != null)

-                {

-                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

-                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, new IdentifierExpr(Token.NoToken,

-                        verifier.MakeThreadId(Token.NoToken, "X")));

+            var bvc = le.Val as BvConst;

+            if (bvc == null)

+                return false;

 

-                    Expr candidateInvariantExpr = Expr.Imp(

-                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

-                            modPow2Expr);

+            return bvc.Value.InInt32 && bvc.Value.ToInt == 1;

+        }

 

-                    AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride local");

-                    return true;

-                }

+        private StrideConstraint BuildAddStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)

+        {

+            if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)

+            {

+                return new EqStrideConstraint(e);

             }

 

-            {

-                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], false, impl);

-                if (constant != null)

-                {

-                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

-                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, verifier.GlobalIdExpr("X"));

+            if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)

+                return BuildAddStrideConstraint(e, rhsc, lhsc);

 

-                    Expr candidateInvariantExpr = Expr.Imp(

-                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

-                            modPow2Expr);

+            if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)

+            {

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsec = (EqStrideConstraint)rhsc;

 

-                    AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride global");

-                    return true;

-                }

+                return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));

             }

 

-            return false;

+            if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint)

+            {

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsmc = (ModStrideConstraint)rhsc;

 

-        }

+                if (lhsmc.mod == rhsmc.mod)

+                    return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));

+            }

 

-        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

-        {

-            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

-            verifier.AddCandidateInvariant(region, candidate, tag);

+            return BuildBottomStrideConstraint(e);

         }

 

-        private Expr IsIdPlusConstantMultiple(Expr arg1, Expr arg2, bool local, Implementation impl)

+        private StrideConstraint BuildMulStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)

         {

+            if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)

             {

-                Expr constant = IsConstantMultiple(arg2);

-                if (constant != null && IsId(arg1, local, impl))

-                {

-                    return constant;

-                }

+                return new EqStrideConstraint(e);

             }

 

+            if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)

+                return BuildMulStrideConstraint(e, rhsc, lhsc);

+

+            if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)

             {

-                Expr constant = IsConstantMultiple(arg1);

-                if (constant != null && IsId(arg2, local, impl))

-                {

-                    return constant;

-                }

-            }

+                var lhsmc = (ModStrideConstraint)lhsc;

+                var rhsec = (EqStrideConstraint)rhsc;

 

-            return null;

+                return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),

+                                               verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));

+            }

 

+            return BuildBottomStrideConstraint(e);

         }

 

-        private Expr IsConstantMultiple(Expr e)

+        private StrideConstraint BuildStrideConstraint(Implementation impl, Expr e)

         {

-            if (!(e is NAryExpr))

-            {

-                return null;

-            }

+            if (e is LiteralExpr || (e is IdentifierExpr && ((IdentifierExpr)e).Decl is Constant))

+                return new EqStrideConstraint(e);

 

-            NAryExpr nary = e as NAryExpr;

+            Expr lhs, rhs;

 

-            if (!(nary.Fun.FunctionName.Equals("BV32_MUL")))

+            if (GPUVerifier.IsBVAdd(e, out lhs, out rhs))

             {

-                return null;

+                var lhsc = BuildStrideConstraint(impl, lhs);

+                var rhsc = BuildStrideConstraint(impl, rhs);

+                return BuildAddStrideConstraint(e, lhsc, rhsc);

             }

 

-            if (IsConstant(nary.Args[0]))

+            if (GPUVerifier.IsBVMul(e, out lhs, out rhs))

             {

-                return nary.Args[0];

+                var lhsc = BuildStrideConstraint(impl, lhs);

+                var rhsc = BuildStrideConstraint(impl, rhs);

+                return BuildMulStrideConstraint(e, lhsc, rhsc);

             }

 

-            if (IsConstant(nary.Args[1]))

-            {

-                return nary.Args[1];

-            }

-

-            return null;

-

+            return BuildBottomStrideConstraint(e);

         }

 

-        private bool IsId(Expr mayBeId, bool local, Implementation impl)

+        private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

         {

-            if (local)

+            bool isConstant;

+            e = verifier.varDefAnalyses[impl].SubstDefinitions(e, impl.Name, out isConstant);

+            if (isConstant)

+                return false;

+

+            var sc = BuildStrideConstraint(impl, e);

+            var msc = sc as ModStrideConstraint;

+            if (msc != null && !IsBottomStrideConstraint(msc))

             {

-                return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, mayBeId);

+                Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

+                Expr modEqExpr = Expr.Eq(verifier.MakeBVURem(offsetExpr, msc.mod), verifier.MakeBVURem(msc.modEq, msc.mod));

+

+                Expr candidateInvariantExpr = Expr.Imp(

+                        new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

+                        modEqExpr);

+

+                AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride");

+                return true;

             }

 

-            return verifier.mayBeGidAnalyser.MayBe("x", impl.Name, mayBeId);

+            return false;

+        }

+

+        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

+        {

+            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

+            verifier.AddCandidateInvariant(region, candidate, tag);

         }

 

         private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

@@ -379,14 +403,14 @@ namespace GPUVerify
                 {

                     if (DoesNotReferTo(nary.Args[0], v))

                     {

-                        return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",

+                        return verifier.MakeBVSub(

                             InverseOfLinearFunctionOfVariable(nary.Args[1], v, offsetExpr),

                             nary.Args[0]);

                     }

                     else

                     {

                         Debug.Assert(DoesNotReferTo(nary.Args[1], v));

-                        return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",

+                        return verifier.MakeBVSub(

                             InverseOfLinearFunctionOfVariable(nary.Args[0], v, offsetExpr),

                             nary.Args[1]);

                     }

@@ -400,11 +424,10 @@ namespace GPUVerify
 

         private Expr ExprModPow2EqualsId(Expr expr, Expr powerOfTwoExpr, Expr threadIdExpr)

         {

-            Expr Pow2Minus1 = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB", powerOfTwoExpr, 

+            Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr, 

                             new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));

 

-            Expr Pow2Minus1BitAndExpr =

-                GPUVerifier.MakeBitVectorBinaryBitVector("BV32_AND", Pow2Minus1, expr);

+            Expr Pow2Minus1BitAndExpr = verifier.MakeBVAnd(Pow2Minus1, expr);

 

             return Expr.Eq(Pow2Minus1BitAndExpr, threadIdExpr);

 

@@ -453,7 +476,7 @@ namespace GPUVerify
         private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)

         {

             var offsets = GetOffsetsAccessed(region, v, accessType)

-               .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))

+               .Select(ofs => verifier.varDefAnalyses[impl].SubstDefinitions(ofs, impl.Name))

                .ToList();

 

             if (offsets.Count != 0 && !offsets.Contains(null))

@@ -520,8 +543,8 @@ namespace GPUVerify
             }

 

             return

-                (SameConstant(nary.Args[0], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[1])) ||

-                (SameConstant(nary.Args[1], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[0]));

+                (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||

+                (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));

         }

 

 

@@ -558,8 +581,8 @@ namespace GPUVerify
             }

 

             return

-                (SameConstant(nary.Args[0], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[1])) ||

-                (SameConstant(nary.Args[1], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[0]));

+                (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||

+                (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));

         }

 

 

diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
index f55e51e8..5dac47d6 100644
--- a/Source/GPUVerify/VariableDefinitionAnalysis.cs
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -5,12 +5,14 @@ using System.Linq;
 

 namespace GPUVerify {

 

+using VarDef = Tuple<Expr, bool>;

+

 class VariableDefinitionAnalysis {

   GPUVerifier verifier;

   Implementation impl;

 

-  Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();

-  Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();

+  Dictionary<Variable, VarDef> defMap = new Dictionary<Variable, VarDef>();

+  Dictionary<string, VarDef> namedDefMap = new Dictionary<string, VarDef>();

   bool changed;

 

   VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {

@@ -19,12 +21,9 @@ class VariableDefinitionAnalysis {
   }

 

   private class IsConstantVisitor : StandardVisitor {

-    private VariableDefinitionAnalysis analysis;

     public bool isConstant = true;

 

-    public IsConstantVisitor(VariableDefinitionAnalysis a) {

-      analysis = a;

-    }

+    public IsConstantVisitor() {}

 

     public override Expr VisitNAryExpr(NAryExpr expr) {

       if (expr.Fun is MapSelect) {

@@ -33,26 +32,48 @@ class VariableDefinitionAnalysis {
       } else

         return base.VisitNAryExpr(expr);

     }

+  };

+

+  private class IsDerivedFromConstantsVisitor : StandardVisitor {

+    private VariableDefinitionAnalysis analysis;

+    public bool isDerivedFromConstants = true;

+

+    public IsDerivedFromConstantsVisitor(VariableDefinitionAnalysis a) {

+      analysis = a;

+    }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

         return expr;

-      if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)

-        isConstant = false;

+      if (!analysis.defMap.ContainsKey(expr.Decl) || !analysis.defMap[expr.Decl].Item2)

+        isDerivedFromConstants = false;

       return expr;

     }

   };

 

   bool IsConstant(Expr e) {

-    var v = new IsConstantVisitor(this);

+    var v = new IsConstantVisitor();

     v.Visit(e);

     return v.isConstant;

   }

 

-  void UpdateDefMap(Variable v, Expr def) {

-    if (!defMap.ContainsKey(v) || defMap[v] != def) {

+  bool IsDerivedFromConstants(Expr e) {

+    var v = new IsDerivedFromConstantsVisitor(this);

+    v.Visit(e);

+    return v.isDerivedFromConstants;

+  }

+

+  void UpdateDefMap(Variable v, Expr def, bool isConstant) {

+    if (!defMap.ContainsKey(v)) {

       changed = true;

-      defMap[v] = def;

+      defMap[v] = new VarDef(def, isConstant);

+      return;

+    }

+

+    var d = defMap[v];

+    if (d.Item1 != def || d.Item2 != isConstant) {

+      changed = true;

+      defMap[v] = new VarDef(def, isConstant);

     }

   }

 

@@ -60,10 +81,10 @@ class VariableDefinitionAnalysis {
     if (lhs is SimpleAssignLhs) {

       var sLhs = (SimpleAssignLhs)lhs;

       var theVar = sLhs.DeepAssignedVariable;

-      if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {

-        UpdateDefMap(theVar, null);

+      if ((defMap.ContainsKey(theVar) && defMap[theVar].Item1 != rhs) || !IsConstant(rhs)) {

+        UpdateDefMap(theVar, null, false);

       } else {

-        UpdateDefMap(theVar, rhs);

+        UpdateDefMap(theVar, rhs, IsDerivedFromConstants(rhs));

       }

     }

   }

@@ -78,11 +99,16 @@ class VariableDefinitionAnalysis {
             AddAssignment(a.Item1, a.Item2);

           }

         }

+        if (c is HavocCmd) {

+          var hCmd = (HavocCmd)c;

+          foreach (Variable v in hCmd.Vars)

+            UpdateDefMap(v, null, false);

+        }

       }

     } while (changed);

   }

 

-  private class BuildNamedDefVisitor : StandardVisitor {

+  private class BuildNamedDefVisitor : Duplicator {

     private VariableDefinitionAnalysis analysis;

 

     public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {

@@ -92,56 +118,79 @@ class VariableDefinitionAnalysis {
     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

         return expr;

-      return analysis.BuildNamedDefFor(expr.Decl);

+      return analysis.BuildNamedDefFor(expr.Decl, expr);

     }

   }

 

-  Expr BuildNamedDefFor(Variable v) {

-    Expr def;

+  Expr BuildNamedDefFor(Variable v, Expr e = null) {

+    VarDef def;

     if (namedDefMap.TryGetValue(v.Name, out def))

-      return def;

-    def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());

-    namedDefMap[v.Name] = def;

-    return def;

+      return def.Item1;

+

+    def = defMap[v];

+    Expr defExpr;

+    if (def.Item1 == null)

+      defExpr = e;

+    else

+      defExpr = (Expr)new BuildNamedDefVisitor(this).Visit(def.Item1.Clone());

+    namedDefMap[v.Name] = new VarDef(defExpr, def.Item2);

+

+    return defExpr;

   }

 

   void BuildNamedDefMap() {

     foreach (var v in defMap.Keys)

-      if (defMap[v] != null)

+      if (defMap[v].Item1 != null)

         BuildNamedDefFor(v);

   }

 

-  private class SubstDualisedDefVisitor : StandardVisitor {

+  private class SubstDefVisitor : Duplicator {

     private VariableDefinitionAnalysis analysis;

-    private VariableDualiser dualiser;

+    private string procName;

     public bool isSubstitutable = true;

+    public bool isConstant = true;

 

-    public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {

+    public SubstDefVisitor(VariableDefinitionAnalysis a, string p) {

       analysis = a;

-      dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);

+      procName = p;

     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

-        return dualiser.VisitIdentifierExpr(expr);

-      var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);

-      Expr def;

+        return expr;

+      int id;

+      var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name, out id);

+      VarDef def;

       if (!analysis.namedDefMap.TryGetValue(varName, out def)) {

         isSubstitutable = false;

         return null;

       }

-      return (Expr)dualiser.Visit(def.Clone());

+      if (!def.Item2)

+        isConstant = false;

+      if (id == 0)

+        return def.Item1;

+      else

+        return (Expr)new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName).Visit(def.Item1.Clone());

     }

   }

 

-  public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {

-    var v = new SubstDualisedDefVisitor(this, id, procName);

+  public Expr SubstDefinitions(Expr e, string procName, out bool isConstant) {

+    var v = new SubstDefVisitor(this, procName);

     Expr result = (Expr)v.Visit(e.Clone());

+    isConstant = v.isConstant;

     if (!v.isSubstitutable)

       return null;

     return result;

   }

 

+  public Expr SubstDefinitions(Expr e, string procName) {

+    bool isConstant;

+    var result = SubstDefinitions(e, procName, out isConstant);

+    if (!isConstant)

+      return null;

+    return result;

+  }

+

   public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {

     var a = new VariableDefinitionAnalysis(verifier, impl);

     a.Analyse();

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 987574be..dcdb087f 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -77,10 +77,14 @@ public class BlockPredicator {
         // the first statement in the block.
         var assign = cmdSeq.Last();
         cmdSeq.Truncate(cmdSeq.Length-1);
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
+        aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
+        cmdSeq.Add(aCmd);
+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
         cmdSeq.Add(assign);
       } else {
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+        aCmd.Expr = Expr.Imp(p, aCmd.Expr);
+        cmdSeq.Add(aCmd);
+        // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
       }
     } else if (cmd is AssumeCmd) {
       var aCmd = (AssumeCmd)cmd;
@@ -114,15 +118,20 @@ public class BlockPredicator {
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
       cmdSeq.Add(cCmd);
-    } else if (cmd is StateCmd) {
-      var sCmd = (StateCmd)cmd;
-      var newCmdSeq = new CmdSeq();
-      foreach (Cmd c in sCmd.Cmds)
-        PredicateCmd(newCmdSeq, c);
-      sCmd.Cmds = newCmdSeq;
-      cmdSeq.Add(sCmd);
-    } else {
-      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+    else if (cmd is CommentCmd) {
+      // skip

+    }

+    else if (cmd is StateCmd) {

+      var sCmd = (StateCmd)cmd;

+      var newCmdSeq = new CmdSeq();

+      foreach (Cmd c in sCmd.Cmds)

+        PredicateCmd(newCmdSeq, c);

+      sCmd.Cmds = newCmdSeq;

+      cmdSeq.Add(sCmd);

+    }

+    else {

+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());

     }
   }
 
@@ -298,13 +307,23 @@ public class BlockPredicator {
         dwf.InParams = new VariableSeq(
           (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
             .ToArray());
-      }
-      var impl = decl as Implementation;
-      if (impl != null)
-        new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
+      }

+      try {

+        var impl = decl as Implementation;

+        if (impl != null)

+          new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();

+      }

+      catch (Program.IrreducibleLoopException) { }
     }
   }
 
+  public static void Predicate(Program p, Implementation impl) {

+    try {

+      new BlockPredicator(p, impl, false, false).PredicateImplementation();

+    }

+    catch (Program.IrreducibleLoopException) { }
+  }
+
 }
 
 }
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 373b685a..1c3fa979 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1968,6 +1968,26 @@ namespace VC {
       #endregion

     }

 

+    public void DesugarCalls(Implementation impl) {

+      foreach (Block block in impl.Blocks) {

+        CmdSeq newCmds = new CmdSeq();

+        foreach (Cmd cmd in block.Cmds) {

+          SugaredCmd sugaredCmd = cmd as SugaredCmd;

+          if (sugaredCmd != null) {

+            StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;

+            foreach (Variable v in stateCmd.Locals) {

+              impl.LocVars.Add(v);

+            }

+            newCmds.AddRange(stateCmd.Cmds);

+          }

+          else {

+            newCmds.Add(cmd);

+          }

+        }

+        block.Cmds = newCmds;

+      }

+    }

+

     public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

@@ -2035,7 +2055,13 @@ namespace VC {
         EmitImpl(impl, true);

       }

       #endregion

-    

+

+      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining == 0) {

+        DesugarCalls(impl);

+        BlockPredicator.Predicate(program, impl);

+        impl.ComputePredecessorsForBlocks();

+      }

+

       if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {

         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }