//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Numerics;
using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using System.Text;
using Microsoft.Boogie;

namespace Microsoft.Dafny {
  public class Translator {
    [NotDelayed]
    public Translator() {
      Bpl.Program boogieProgram = ReadPrelude();
      if (boogieProgram != null) {
        sink = boogieProgram;
        predef = FindPredefinedDecls(boogieProgram);
      }
      base();
      if (predef != null) {
        cevVariables.Add(predef.HeapVarName, predef.CevHeapName);
      }
    }
    
    // translation state
    readonly Dictionary<TopLevelDecl!,Bpl.Constant!>! classes = new Dictionary<TopLevelDecl!,Bpl.Constant!>();
    readonly Dictionary<Field!,Bpl.Constant!>! fields = new Dictionary<Field!,Bpl.Constant!>();

    // Machinery for providing information to the Counterexample Visualizer
    readonly Dictionary<string!,int>! cevFilenames = new Dictionary<string!,int>();
    readonly Dictionary<IToken!,Bpl.Constant!>! cevLocations = new Dictionary<IToken!,Bpl.Constant!>();
    readonly Dictionary<string!,Bpl.Constant!>! cevVariables = new Dictionary<string!,Bpl.Constant!>();
    Bpl.Expr! CevLocation(IToken! tok)
      requires predef != null && sink != null;
    {
      Bpl.Constant c;
      if (cevLocations.TryGetValue(tok, out c)) {
        assert c != null;
      } else {
        int fileId;
        string filename = "#file^" + (tok.filename == null ? ".dfy" : tok.filename);
        if (!cevFilenames.TryGetValue(filename, out fileId)) {
          fileId = cevFilenames.Count;
          cevFilenames.Add(filename, fileId);
          Bpl.Constant fn = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, Sanitize(filename), predef.CevTokenType), true);
          sink.TopLevelDeclarations.Add(fn);
          sink.TopLevelDeclarations.Add(new Bpl.Axiom(tok, FunctionCall(tok, "$file_name_is", Bpl.Type.Bool, Bpl.Expr.Literal(fileId), new Bpl.IdentifierExpr(tok, fn))));
        }
        c = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, string.Format("#tok${0}^{1}.{2}", fileId, tok.line, tok.col), predef.CevTokenType), true);
        cevLocations.Add(tok, c);
        sink.TopLevelDeclarations.Add(c);
      }
      return new Bpl.IdentifierExpr(tok, c);
    }
    static string! Sanitize(string! s) {
      StringBuilder sb = new StringBuilder();
      foreach (char ch in s) {
        if (char.IsLetterOrDigit(ch) || ch == '#' || ch == '^' || ch == '$' || ch == '.' || ch == '@') {
          sb.Append(ch);
        } else {
          sb.Append(string.Format("%{0:X4}", (int)ch));
        }
      }
      return sb.ToString();
    }
    Bpl.Expr! CevVariable(Bpl.IToken! tok, string! name)
      requires predef != null && sink != null;
    {
      Bpl.Constant c;
      if (cevVariables.TryGetValue(name, out c)) {
        assert c != null;
      } else {
        c = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, string.Format("#loc.{0}", name), predef.CevTokenType), true);
        cevVariables.Add(name, c);
        sink.TopLevelDeclarations.Add(c);
      }
      return new Bpl.IdentifierExpr(tok, c);
    }
    
    readonly Bpl.Program sink;
    readonly PredefinedDecls predef;
    internal class PredefinedDecls {
      public readonly Bpl.Type! RefType;
      public readonly Bpl.Type! BoxType;
      public readonly Bpl.Type! CevTokenType;
      public readonly Bpl.Type! CevVariableKind;
      public readonly Bpl.Type! CevEventType;
      private readonly Bpl.TypeSynonymDecl! setTypeCtor;
      public Bpl.Type! SetType(IToken! tok, Bpl.Type! ty) {
        return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
      }
      private readonly Bpl.TypeCtorDecl! seqTypeCtor;
      public Bpl.Type! SeqType(IToken! tok, Bpl.Type! ty) {
        return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
      }
      readonly Bpl.TypeCtorDecl! fieldName;
      public Bpl.Type! FieldName(IToken! tok, Bpl.Type! ty) {
        return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));
      }
      public readonly Bpl.Type! HeapType;
      public readonly string! HeapVarName;
      public readonly Bpl.Constant! CevHeapName;
      public readonly Bpl.Type! ClassNameType;
      public readonly Bpl.Type! FieldCategoryType;
      public readonly Bpl.Type! DatatypeType;
      public readonly Bpl.Type! DtCtorId;
      public readonly Bpl.Expr! Null;
      private readonly Bpl.Constant! allocField;
      public Bpl.IdentifierExpr! Alloc(IToken! tok) {
        return new Bpl.IdentifierExpr(tok, allocField);
      }

      public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
                             Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
                             Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! fieldCategoryType,
                             Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
                             Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
        Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
        this.RefType = refT;
        this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
        this.CevTokenType = new Bpl.CtorType(Token.NoToken, cevTokenType, new Bpl.TypeSeq());
        this.CevVariableKind = new Bpl.CtorType(Token.NoToken, cevVariableKind, new Bpl.TypeSeq());
        this.CevEventType = new Bpl.CtorType(Token.NoToken, cevEventType, new Bpl.TypeSeq());
        this.setTypeCtor = setTypeCtor;
        this.seqTypeCtor = seqTypeCtor;
        this.fieldName = fieldNameType;
        this.HeapType = heap.TypedIdent.Type;
        this.HeapVarName = heap.Name;
        this.CevHeapName = cevHeapNameConst;
        this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
        this.FieldCategoryType = new Bpl.CtorType(Token.NoToken, fieldCategoryType, new Bpl.TypeSeq());
        this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
        this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
        this.allocField = allocField;
        this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
      }
    }
    
    static PredefinedDecls FindPredefinedDecls(Bpl.Program! prog) {
      if (prog.Resolve() != 0) {
        Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
        return null;
      }
      
      Bpl.TypeCtorDecl refType = null;
      Bpl.TypeCtorDecl cevTokenType = null;
      Bpl.TypeCtorDecl cevVariableKind = null;
      Bpl.TypeCtorDecl cevEventType = null;
      Bpl.TypeSynonymDecl setTypeCtor = null;
      Bpl.TypeCtorDecl seqTypeCtor = null;
      Bpl.TypeCtorDecl fieldNameType = null;
      Bpl.TypeCtorDecl classNameType = null;
      Bpl.TypeCtorDecl fieldCategoryType = null;
      Bpl.TypeCtorDecl datatypeType = null;
      Bpl.TypeCtorDecl dtCtorId = null;
      Bpl.TypeCtorDecl boxType = null;
      Bpl.GlobalVariable heap = null;
      Bpl.Constant allocField = null;
      Bpl.Constant cevHeapNameConst = null;
      foreach (Bpl.Declaration d in prog.TopLevelDeclarations) {
        if (d is Bpl.TypeCtorDecl) {
          Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
          if (dt.Name == "Seq") {
            seqTypeCtor = dt;
          } else if (dt.Name == "Field") {
            fieldNameType = dt;
          } else if (dt.Name == "ClassName") {
            classNameType = dt;
          } else if (dt.Name == "FieldCategory") {
            fieldCategoryType = dt;
          } else if (dt.Name == "DatatypeType") {
            datatypeType = dt;
          } else if (dt.Name == "DtCtorId") {
            dtCtorId = dt;
          } else if (dt.Name == "ref") {
            refType = dt;
          } else if (dt.Name == "BoxType") {
            boxType = dt;
          } else if (dt.Name == "$token") {
            cevTokenType = dt;
          } else if (dt.Name == "var_locglob") {
            cevVariableKind = dt;
          } else if (dt.Name == "cf_event") {
            cevEventType = dt;
          }
        } else if (d is Bpl.TypeSynonymDecl) {
          Bpl.TypeSynonymDecl dt = (Bpl.TypeSynonymDecl)d;
          if (dt.Name == "Set") {
            setTypeCtor = dt;
          }
        } else if (d is Bpl.Constant) {
          Bpl.Constant c = (Bpl.Constant)d;
          if (c.Name == "alloc") {
            allocField = c;
          } else if (c.Name == "#loc.$Heap") {
            cevHeapNameConst = c;
          }
        } else if (d is Bpl.GlobalVariable) {
          Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;
          if (v.Name == "$Heap") {
            heap = v;
          }
        }
      }
      if (seqTypeCtor == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq");
      } else if (setTypeCtor == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
      } else if (fieldNameType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
      } else if (classNameType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
      } else if (fieldCategoryType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type FieldCategory");
      } else if (datatypeType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
      } else if (dtCtorId == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type DtCtorId");
      } else if (refType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
      } else if (boxType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type BoxType");
      } else if (cevTokenType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type $token");
      } else if (cevVariableKind == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type var_locglob");
      } else if (cevEventType == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of type cf_event");
      } else if (heap == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");
      } else if (allocField == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
      } else if (cevHeapNameConst == null) {
        Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
      } else {
        return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
                                   setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, fieldCategoryType, datatypeType, dtCtorId,
                                   allocField, cevHeapNameConst);
      }
      return null;
    }
    
    static Bpl.Program ReadPrelude() {
      //using (System.IO.Stream stream = (!) System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource
      string! codebase = (!) System.IO.Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
      string! preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");
      
      Bpl.Program prelude;
      int errorCount = Bpl.Parser.Parse(preludePath, out prelude);
      if (prelude == null || errorCount > 0) {
        return null;
      } else {
        return prelude;
      }
/*      
      List<string!> defines = new List<string!>();
      using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))
      {
        BoogiePL.Buffer.Fill(new System.IO.StreamReader(stream), defines);
        //BoogiePL.Scanner.Init("<DafnyPrelude.bpl>");
        Bpl.Program prelude;
        int errorCount = BoogiePL.Parser.Parse(out prelude);
        if (prelude == null || errorCount > 0) {
          return null;
        } else {
          return prelude;
        }
      }
*/      
    }
    
    public Bpl.Program! Translate(Program! program) {
      if (sink == null || predef == null) {
        // something went wrong during construction, which reads the prelude; an error has
        // already been printed, so just return an empty program here (which is non-null)
        return new Bpl.Program();
      }
      foreach (ModuleDecl m in program.Modules) {
        foreach (TopLevelDecl d in m.TopLevelDecls) {
          if (d is DatatypeDecl) {
            AddDatatype((DatatypeDecl)d);
          } else {
            AddClassMembers((ClassDecl)d);
          }
        }
      }
      return sink;
    }
    
    void AddDatatype(DatatypeDecl! dt)
      requires sink != null && predef != null;
    {
      foreach (DatatypeCtor ctor in dt.Ctors) {
        // Add:  function #dt.ctor(paramTypes) returns (DatatypeType);
        Bpl.VariableSeq argTypes = new Bpl.VariableSeq();
        foreach (Formal arg in ctor.Formals) {
          Bpl.Variable a = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), true);
          argTypes.Add(a);
        }
        Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);
        Bpl.Function fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType);
        sink.TopLevelDeclarations.Add(fn);
        // Add:  const unique ##dt.ctor: DtCtorId;
        Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);
        sink.TopLevelDeclarations.Add(cid);
        // Add:  axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);
        Bpl.VariableSeq! bvs;
        List<Bpl.Expr!>! args;
        CreateBoundVariables(ctor.Formals, out bvs, out args);
        Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
        lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);
        Bpl.Expr q = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));
        if (bvs.Length != 0) {
          q = new Bpl.ForallExpr(ctor.tok, bvs, q);
        }
        sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
        // Add injectivity axioms:
        int i = 0;
        foreach (Formal arg in ctor.Formals) {
          // function ##dt.ctor#i(DatatypeType) returns (Ti);
          argTypes = new Bpl.VariableSeq();
          argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true));
          resType = new Bpl.Formal(arg.tok, new Bpl.TypedIdent(arg.tok, Bpl.TypedIdent.NoName, TrType(arg.Type)), false);
          fn = new Bpl.Function(ctor.tok, "#" + ctor.FullName + "#" + i, argTypes, resType);
          sink.TopLevelDeclarations.Add(fn);
          // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);
          CreateBoundVariables(ctor.Formals, out bvs, out args);
          lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
          lhs = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), lhs);
          q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Eq(lhs, args[i]));
          sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
          if (arg.Type.IsDatatype || arg.Type.IsTypeParameter) {
            // for datatype:             axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));
            // for type-parameter type:  axiom (forall params :: DtRank(Unbox(params_i)) < DtRank(#dt.ctor(params)));
            CreateBoundVariables(ctor.Formals, out bvs, out args);
            lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
              arg.Type.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i]));
            Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
            rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
            q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));
            sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
          } else if (arg.Type is SeqType) {
            // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params)));
            // that is:
            // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params)));
            CreateBoundVariables(ctor.Formals, out bvs, out args);
            Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));
            bvs.Add(iVar);
            Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);
            Bpl.Expr ante = Bpl.Expr.And(
              Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),
              Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));
            lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,
              FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType,
                FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie)));
            Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
            rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
            q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
            sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
          } else if (arg.Type is SetType) {
            // axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
            // that is:
            // axiom (forall params, d: Datatype :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
            CreateBoundVariables(ctor.Formals, out bvs, out args);
            Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));
            bvs.Add(dVar);
            Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);
            Bpl.Expr ante = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));
            lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
            Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
            rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
            q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
            sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
          }
          i++;
        }
      }
    }
    
    void CreateBoundVariables(List<Formal!>! formals, out Bpl.VariableSeq! bvs, out List<Bpl.Expr!>! args)
      ensures bvs.Length == args.Count;
    {
      bvs = new Bpl.VariableSeq();
      args = new List<Bpl.Expr!>();
      foreach (Formal arg in formals) {
        Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "a" + bvs.Length, TrType(arg.Type)));
        bvs.Add(bv);
        args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
      }
    }
    
    void AddClassMembers(ClassDecl! c)
      requires sink != null && predef != null;
    {
      sink.TopLevelDeclarations.Add(GetClass(c));
      
      foreach (MemberDecl member in c.Members) {
        if (member is Field) {
          Field f = (Field)member;
          Bpl.Constant fc = GetField(f);
          sink.TopLevelDeclarations.Add(fc);
          
          AddAllocationAxiom(f);
          
        } else if (member is Function) {
          Function f = (Function)member;
          AddFunction(f);
          if (f.Body != null) {
            if (f.Body is MatchExpr) {
              MatchExpr me = (MatchExpr)f.Body;
              Formal formal = (Formal)((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks
              foreach (MatchCaseExpr mc in me.Cases) {
                assert mc.Ctor != null;  // the field is filled in by resolution
                Bpl.Axiom ax = FunctionAxiom(f, mc.Body, formal, mc.Ctor, mc.Arguments);
                sink.TopLevelDeclarations.Add(ax);
              }
            } else {
              Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);
              sink.TopLevelDeclarations.Add(ax);
            }
            if (f.IsRecursive && !f.IsUnlimited) {
              AddLimitedAxioms(f);
            }
          }
          AddFrameAxiom(f);
          AddWellformednessCheck(f);
          
        } else if (member is Method) {
          Method m = (Method)member;
          // wellformedness check for method specification
          Bpl.Procedure proc = AddMethod(m, true);
          AddMethodImpl(m, proc, true);
          // the method itself
          proc = AddMethod(m, false);
          if (m.Body != null) {
            // ...and its implementation
            AddMethodImpl(m, proc, false);
          }

        } else {
          assert false;  // unexpected member
        }
      }
    }
    
    Bpl.Axiom! FunctionAxiom(Function! f, Expression! body, Formal specializationFormal,
                             DatatypeCtor ctor, List<BoundVar!> specializationReplacementFormals)
      requires predef != null;
      requires specializationFormal == null <==> ctor == null;
      requires specializationFormal == null <==> specializationReplacementFormals == null;
      requires f.EnclosingClass != null;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
      
      // axiom
      //   mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))
      //   ==>
      //   (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body);
      //
      // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
      // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by
      // "specializationReplacementFormals".
      // The list "args" is the list of formals of function "f"; except, if a specialization is provided, then
      // "specializationFormal" is replaced by the expression "ctor(specializationReplacementFormals)".
      // If a specialization is provided, occurrences of "specializationFormal" in "body" are also replaced by
      // that expression.
      //
      // The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
      //
      // Note, an antecedent $Heap[this,alloc] is intentionally left out:  including it would only weaken
      // the axiom.  Moreover, leaving it out does not introduce any soundness problem, because the Dafny
      // allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
      // sound after that, then it would also have been sound just before the allocation.
      //
      Bpl.VariableSeq formals = new Bpl.VariableSeq();
      Bpl.ExprSeq args = new Bpl.ExprSeq();
      Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
      formals.Add(bv);
      args.Add(new Bpl.IdentifierExpr(f.tok, bv));
      Bpl.BoundVariable bvThis;
      Bpl.Expr bvThisIdExpr;
      if (f.IsStatic) {
        bvThis = null;
        bvThisIdExpr = null;
      } else {
        bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
        formals.Add(bvThis);
        bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
        args.Add(bvThisIdExpr);
      }
      DatatypeValue r = null;
      if (specializationReplacementFormals != null) {
        assert ctor != null;  // follows from if guard and the precondition
        List<Expression!> rArgs = new List<Expression!>();
        foreach (BoundVar p in specializationReplacementFormals) {
          bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
          formals.Add(bv);
          IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
          ie.Var = p;  ie.Type = ie.Var.Type;  // resolve it here
          rArgs.Add(ie);
        }
        r = new DatatypeValue(f.tok, ((!)ctor.EnclosingDatatype).Name, ctor.Name, rArgs);
        r.Ctor = ctor;  r.Type = new UserDefinedType(f.tok, ctor.EnclosingDatatype.Name, new List<Type!>()/*this is not right, but it seems like it won't matter here*/);  // resolve it here
      }
      foreach (Formal p in f.Formals) {
        if (p != specializationFormal) {
          bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
          formals.Add(bv);
          args.Add(new Bpl.IdentifierExpr(p.tok, bv));
        } else {
          assert r != null;  // it is set above
          args.Add(etran.TrExpr(r));
        }
      }

      // mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh < FunctionContextHeight || InMethodContext))
      ModuleDecl m = f.EnclosingClass.Module;
      Bpl.Expr activate = Bpl.Expr.Or(
        Bpl.Expr.Lt(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),
        Bpl.Expr.And(
          Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),
          Bpl.Expr.Or(
            Bpl.Expr.Lt(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),
            etran.InMethodContext())));
      
      Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
      if (!f.IsStatic) {
        assert bvThisIdExpr != null;  // set to non-null value above when !f.IsStatic
        ante = Bpl.Expr.And(ante, Bpl.Expr.Neq(bvThisIdExpr, predef.Null));
      }
      foreach (Expression req in f.Req) {
        ante = Bpl.Expr.And(ante, etran.TrExpr(req));
      }
      Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
      Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
      Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
      if (specializationFormal != null) {
        assert r != null;
        Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
        substMap.Add(specializationFormal, r);
        body = Substitute(body, null, substMap);
      }
      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(body))));
      return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax));
    }
    
    void AddLimitedAxioms(Function! f)
      requires f.IsRecursive && !f.IsUnlimited;
      requires sink != null && predef != null;
    {
      // axiom (forall formals :: { f(args) } f(args) == f#limited(args))

      Bpl.VariableSeq formals = new Bpl.VariableSeq();
      Bpl.ExprSeq args = new Bpl.ExprSeq();
      Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
      formals.Add(bv);
      args.Add(new Bpl.IdentifierExpr(f.tok, bv));
      Bpl.BoundVariable bvThis;
      Bpl.Expr bvThisIdExpr;
      if (f.IsStatic) {
        bvThis = null;
        bvThisIdExpr = null;
      } else {
        bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
        formals.Add(bvThis);
        bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
        args.Add(bvThisIdExpr);
      }
      foreach (Formal p in f.Formals) {
        bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
        formals.Add(bv);
        args.Add(new Bpl.IdentifierExpr(p.tok, bv));
      }
      
      Bpl.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
      Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
      Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
      Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
      
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

      Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, limitedFuncAppl));
      sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
    }
    
    void AddAllocationAxiom(Field! f)
      requires sink != null && predef != null;
    {
      if (f.Type is BoolType || f.Type is IntType || f.Type.IsTypeParameter) {
        return;
      }
      
      Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));
      Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);
      Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
      Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
      
      // h[o,f]
      Bpl.Expr oDotF = Bpl.Expr.SelectTok(f.tok, h, o, new Bpl.IdentifierExpr(f.tok, GetField(f)));
      // $IsGoodHeap(h) && o != null && h[o,alloc]
      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.And(
        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, h),
        Bpl.Expr.Neq(o, predef.Null)),
        etran.IsAlloced(f.tok, o));

      if (f.Type is SetType) {
        SetType st = (SetType)f.Type;
        if (st.Arg.IsRefType) {
          //   axiom (forall h: [ref, Field x]x, o: ref, t: BoxType ::
          //        { h[o,f][t] }
          //        $IsGoodHeap(h) && o != null && h[o,alloc] && h[o,f][t] ==> UnBox(t) == null || h[UnBox(t), alloc]);
          Bpl.BoundVariable tVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$t", predef.BoxType));
          Bpl.Expr t = new Bpl.IdentifierExpr(f.tok, tVar);
          Bpl.Expr oDotFsubT = Bpl.Expr.SelectTok(f.tok, oDotF, t);
          Bpl.Expr unboxT = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, t);

          Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubT));
          
          Bpl.Expr goodRef = etran.GoodRef(f.tok, unboxT, st.Arg);
          Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, oDotFsubT), Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));
          Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, tVar), tr, body);
          sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
        } else {
          // TODO: should also handle sets of sets, etc.  This will probably require some extra predicates, and these predicates may even replace the above treatment of sets.
        }
        
      } else if (f.Type is SeqType) {
        SeqType st = (SeqType)f.Type;
        if (st.Arg.IsRefType) {
          //   axiom (forall h: [ref, Field x]x, o: ref, i: int ::
          //        { Seq#Index(h[o,f], i) }
          //        $IsGoodHeap(h) && o != null && h[o,alloc] && 0 <= i && i < Seq#Length(h[o,f]) ==> Unbox(Seq#Index(h[o,f], i)) == null || h[Unbox(Seq#Index(h[o,f], i)), alloc]);
          Bpl.BoundVariable iVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$i", Bpl.Type.Int));
          Bpl.Expr i = new Bpl.IdentifierExpr(f.tok, iVar);
          Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.BoxType, oDotF, i);
          Bpl.Expr unbox = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, oDotFsubI);
          
          Bpl.Expr range = InSeqRange(f.tok, i, oDotF, true, null, false);
          
          Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubI));
          
          Bpl.Expr goodRef = etran.GoodRef(f.tok, unbox, st.Arg);
          Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, range), Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));
          Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, iVar), tr, body);
          sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
        } else {
          // TODO: should also handle sequences of sequences, etc.  This will probably require some extra predicates, and these predicates may even replace the above treatment of sequences.
        }
      
      } else if (f.Type.IsDatatype) {
        // TODO
        
      } else {
        // reference type:
        //   axiom (forall h: [ref, Field x]x, o: ref ::
        //        { h[o,f] }
        //        $IsGoodHeap(h) && o != null && h[o,alloc] ==> h[o,f] == null || h[h[o,f], alloc]);
        Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF));
        
        Bpl.Expr goodRef = etran.GoodRef(f.tok, oDotF, f.Type);
        Bpl.Expr body = Bpl.Expr.Imp(ante, Bpl.Expr.Or(Bpl.Expr.Eq(oDotF, predef.Null), goodRef));
        Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar), tr, body);
        sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
      }
    }

    Bpl.Expr! InSeqRange(IToken! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
      if (lowerBound == null) {
        lowerBound = Bpl.Expr.Literal(0);
      }
      Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
      Bpl.Expr length = FunctionCall(tok, isSequence ? BuiltinFunction.SeqLength : BuiltinFunction.ArrayLength, null, seq);
      Bpl.Expr upper;
      if (includeUpperBound) {
        upper = Bpl.Expr.Le(index, length);
      } else {
        upper = Bpl.Expr.Lt(index, length);
      }
      return Bpl.Expr.And(lower, upper);
    }
    
    Method currentMethod = null;  // the method whose implementation is currently being translated
    int loopHeapVarCount = 0;
    int otherTmpVarCount = 0;
    Bpl.IdentifierExpr _phvie = null;
    Bpl.IdentifierExpr! GetPrevHeapVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it
      requires predef != null;
    {
      if (_phvie == null) {
        // the "tok" of the first request for this variable is the one we use
        Bpl.LocalVariable prevHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$prevHeap", predef.HeapType));
        locals.Add(prevHeapVar);
        _phvie = new Bpl.IdentifierExpr(tok, prevHeapVar);
      }
      return _phvie;
    }
    Bpl.IdentifierExpr _nwie = null;
    Bpl.IdentifierExpr! GetNewVar_IdExpr(IToken! tok, Bpl.VariableSeq! locals)  // local variable that's shared between statements that need it
      requires predef != null;
    {
      if (_nwie == null) {
        // the "tok" of the first request for this variable is the one we use
        Bpl.LocalVariable nwVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$nw", predef.RefType));  // important: no where clause (that's why we're going through the trouble of setting of this variable in the first place)
        locals.Add(nwVar);
        _nwie = new Bpl.IdentifierExpr(tok, nwVar);
      }
      return _nwie;
    }

    void AddMethodImpl(Method! m, Bpl.Procedure! proc, bool wellformednessProc)
      requires sink != null && predef != null;
      requires wellformednessProc || m.Body != null;
      requires currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null;
      ensures currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null;
    {
      currentMethod = m;

      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
      Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);
      Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
      Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
      GenerateImplPrelude(m, inParams, outParams, builder, localVariables);
      Bpl.StmtList stmts;
      if (!wellformednessProc) {
        // translate the body of the method
        assert m.Body != null;  // follows from method precondition and the if guard
        stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);
      } else {
        // check well-formedness of the preconditions, and then assume each one of them
        foreach (MaybeFreeExpression p in m.Req) {
          CheckWellformed(p.E, null, Position.Positive, localVariables, builder, etran);
          builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
        }
        // Note: the modifies clauses are not checked for well-formedness (is that sound?), because it used to
        // be that the syntax was not rich enough for programmers to specify modifies clauses and always being
        // absolutely well-defined.
        // check well-formedness of the decreases clauses
        foreach (Expression p in m.Decreases) {
          CheckWellformed(p, null, Position.Positive, localVariables, builder, etran);
        }

        // play havoc with the heap according to the modifies clause
        builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
        // assume (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] } $_Frame[o] || $Heap[o,f] == old($Heap)[o,f]);
        Bpl.TypeVariable alpha = new Bpl.TypeVariable(m.tok, "alpha");
        Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));
        Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(m.tok, oVar);
        Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));
        Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(m.tok, fVar);
      
        Bpl.Expr heapOF = Bpl.Expr.SelectTok(m.tok, etran.HeapExpr, o, f);
        Bpl.Expr oldHeapOF = Bpl.Expr.SelectTok(m.tok, etran.Old.HeapExpr, o, f);
        Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.Old.TheFrame(m.tok), o, f);
        Bpl.Expr body = Bpl.Expr.Or(inEnclosingFrame, Bpl.Expr.Eq(heapOF, oldHeapOF));
        Bpl.Trigger tr = new Bpl.Trigger(m.tok, true, new Bpl.ExprSeq(heapOF));
        Bpl.Expr qq = new Bpl.ForallExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, body);
        builder.Add(new Bpl.AssumeCmd(m.tok, qq));

        // also play havoc with the out parameters
        if (outParams.Length != 0) {  // don't create an empty havoc statement
          Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
          foreach (Bpl.Variable! f in outParams) {
            outH.Add(new Bpl.IdentifierExpr(f.tok, f));
          }
          builder.Add(new Bpl.HavocCmd(m.tok, outH));
        }

        // check wellformedness of postconditions
        foreach (MaybeFreeExpression p in m.Ens) {
          CheckWellformed(p.E, null, Position.Positive, localVariables, builder, etran);
          builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));
        }

        stmts = builder.Collect(m.tok);
      }

      Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
        typeParams, inParams, outParams,
        localVariables, stmts);
      sink.TopLevelDeclarations.Add(impl);
      
      currentMethod = null;
      loopHeapVarCount = 0;
      otherTmpVarCount = 0;
      _phvie = null;
      _nwie = null;
    }

    void GenerateImplPrelude(Method! m, Bpl.VariableSeq! inParams, Bpl.VariableSeq! outParams,
                             Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
      requires predef != null;
    {
      // Add CEV prelude
      builder.Add(Bpl.Cmd.SimpleAssign(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(1))));
      foreach (Bpl.Variable p in inParams) {
        assert p != null;
        builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
          new Bpl.ExprSeq(
            CevLocation(p.tok),
            new Bpl.IdentifierExpr(p.tok, "cev_parameter", predef.CevVariableKind),
            CevVariable(p.tok, p.Name),
            new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)),  // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param
          new Bpl.IdentifierExprSeq()));
      }
      foreach (Bpl.Variable p in outParams) {
        assert p != null;
        builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
          new Bpl.ExprSeq(
            CevLocation(p.tok),
            new Bpl.IdentifierExpr(p.tok, "cev_local", predef.CevVariableKind),  // treat out-parameters as locals
            CevVariable(p.tok, p.Name),
            new Bpl.IdentifierExpr(p.tok, p.Name, p.TypedIdent.Type)),  // it's important not to pass in just p, because that resolves to the proc's param, not the impl's param
          new Bpl.IdentifierExprSeq()));
      }

      // set up the information used to verify the method's modifies clause
      DefineFrame(m.tok, m.Mod, builder, localVariables);
    }
    
    void DefineFrame(IToken! tok, List<FrameExpression!>! frameClause, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! localVariables)
      requires predef != null;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);
      // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
      Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
      assert theFrame.Type != null;  // follows from the postcondition of TheFrame
      Bpl.LocalVariable frame = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, theFrame.Name, theFrame.Type));
      localVariables.Add(frame);
      // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause);
      Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
      Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
      Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
      Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
      Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
      Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);
      Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,
                                           Bpl.Expr.Imp(ante, consequent));
    
      builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
    }

    void CheckFrameSubset(IToken! tok, List<FrameExpression!>! calleeFrame,
                          Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap,
                          ExpressionTranslator! etran, Bpl.StmtListBuilder! builder, string! errorMessage)
      requires predef != null;
    {
      // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);
      Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
      Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
      Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
      Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
      Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o));
      Bpl.Expr oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap);
      Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(tok), o, f);
      Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar),
                                      Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));
      builder.Add(Assert(tok, q, errorMessage));
    }
    
    /// <summary>
    /// Generates:
    ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::
    ///        { HeapSucc(h0,h1), F(h1,formals) }
    ///        heaps are well-formed and formals are allocated AND
    ///        HeapSucc(h0,h1)
    ///        AND
    ///        (forall(alpha) o: ref, f: Field alpha ::
    ///            o != null AND h0[o,alloc] AND h1[o,alloc] AND
    ///            o in reads clause of formals in h0
    ///            IMPLIES h0[o,f] == h1[o,f])
    ///        IMPLIES
    ///        F(h0,formals) == F(h1,formals)
    ///      );
    ///
    /// If the function is a recursive, non-unlimited function, then the same axiom is also produced for "F#limited" instead of "F".
    /// </summary>
    void AddFrameAxiom(Function! f)
      requires sink != null && predef != null;
    {
      Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));
      Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));
      Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);
      Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);
      ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);
      ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);
      
      Bpl.Expr wellFormed = Bpl.Expr.And(
        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),
        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));
      
      Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");
      Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
      Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
      Bpl.BoundVariable fieldVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$f", predef.FieldName(f.tok, alpha)));
      Bpl.Expr field = new Bpl.IdentifierExpr(f.tok, fieldVar);
      Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
      Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));
      Bpl.Expr unchanged = Bpl.Expr.Eq(Bpl.Expr.SelectTok(f.tok, h0, o, field), Bpl.Expr.SelectTok(f.tok, h1, o, field));
      
      Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);
      Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);
      Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
        Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
      
      // bvars:  h0, h1, formals
      // f0args:  h0, formals
      // f1args:  h1, formals
      Bpl.VariableSeq bvars = new Bpl.VariableSeq();
      Bpl.ExprSeq f0args = new Bpl.ExprSeq();
      Bpl.ExprSeq f1args = new Bpl.ExprSeq();
      bvars.Add(h0Var);  bvars.Add(h1Var);
      f0args.Add(h0);
      f1args.Add(h1);
      if (!f.IsStatic) {
        Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
        Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar);
        bvars.Add(thVar);
        f0args.Add(th);
        f1args.Add(th);

        Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);
        Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),
          Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));
        wellFormed = Bpl.Expr.And(wellFormed, wh);
      }

      foreach (Formal p in f.Formals) {
        Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
        bvars.Add(bv);
        Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
        f0args.Add(formal);
        f1args.Add(formal);
        Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran0);
        if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
        wh = GetWhereClause(p.tok, formal, p.Type, etran1);
        if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
      }
      
      string axiomComment = "frame axiom for " + f.FullName;
      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
      while (fn != null) {
        Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
        Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
        Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
        Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));
        
        Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
        Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
          Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),
          Bpl.Expr.Imp(q0, eq)));
        sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, axiomComment));
        if (axiomComment != null && f.IsRecursive && !f.IsUnlimited) {
          fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
          axiomComment = null;  // the comment goes only with the first frame axiom
        } else {
          break;  // no more frame axioms to produce
        }
      }
    }
    
    Bpl.Expr! InRWClause(IToken! tok, Bpl.Expr! o, Bpl.Expr! f, List<FrameExpression!>! rw, ExpressionTranslator! etran,
                         Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)
      requires predef != null;
      // requires o to denote an expression of type RefType
      // "rw" is is allowed to contain a WildcardExpr
      requires receiverReplacement == null <==> substMap == null;
    {
      Bpl.Expr disjunction = null;
      foreach (FrameExpression rwComponent in rw) {
        Expression e = rwComponent.E;
        if (substMap != null) {
          assert receiverReplacement != null;
          e = Substitute(e, receiverReplacement, substMap);
        }
        Bpl.Expr disjunct;
        if (e is WildcardExpr) {
          disjunct = Bpl.Expr.True;
        } else if (e.Type is SetType) {
          // old(e)[Box(o)]
          disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg);
        } else if (e.Type is SeqType) {
          // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) && Seq#Index(old(e),i) == Box(o))
          Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);
          Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
          Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
          Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), true, null, false);
          Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i);
          // TODO: the equality in the next line should be changed to one that understands extensionality
          disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.And(iBounds, Bpl.Expr.Eq(XsubI, boxO)));
        } else {
          // o == old(e)
          disjunct = Bpl.Expr.Eq(o, etran.TrExpr(e));
        }
        disjunct = Bpl.Expr.And(IsTotal(e, etran), disjunct);
        if (rwComponent.Field != null) {
          disjunct = Bpl.Expr.And(disjunct, Bpl.Expr.Eq(f, new Bpl.IdentifierExpr(rwComponent.E.tok, GetField(rwComponent.Field))));
        }
        if (disjunction == null) {
          disjunction = disjunct;
        } else {
          disjunction = Bpl.Expr.Or(disjunction, disjunct);
        }
      }
      if (disjunction == null) {
        return Bpl.Expr.False;
      } else {
        return disjunction;
      }
    }
    
    void AddWellformednessCheck(Function! f)
      requires sink != null && predef != null;
      requires f.EnclosingClass != null;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
      // parameters of the procedure
      Bpl.VariableSeq inParams = new Bpl.VariableSeq();
      if (!f.IsStatic) {
        Bpl.Expr wh = Bpl.Expr.And(
          Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),
          etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, f.EnclosingClass)));
        Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType, wh), true);
        inParams.Add(thVar);
      }
      foreach (Formal p in f.Formals) {
        Bpl.Type varType = TrType(p.Type);
        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
        inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
      }
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
      // the procedure itself
      Bpl.RequiresSeq req = new Bpl.RequiresSeq();
      // free requires mh < ModuleContextHeight || (mh == ModuleContextHeight && fh < FunctionContextHeight);
      ModuleDecl m = f.EnclosingClass.Module;
      Bpl.Expr context = Bpl.Expr.And(
        Bpl.Expr.Eq(Bpl.Expr.Literal(m.Height), etran.ModuleContextHeight()),
        Bpl.Expr.Eq(Bpl.Expr.Literal(m.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
      req.Add(Requires(f.tok, true, context, null, null));
      Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
        req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
      sink.TopLevelDeclarations.Add(proc);

      Bpl.VariableSeq locals = new Bpl.VariableSeq();
      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
      // todo: include CEV information of parameters and the heap
      
      // check well-formedness of the preconditions, and then assume each one of them
      foreach (Expression p in f.Req) {
        // Note, in this well-formedness check, function is passed in as null.  This will cause there to be
        // no reads checks or decreases checks.  This seems like a good idea, and I hope it is also sound.
        CheckWellformed(p, null, Position.Positive, locals, builder, etran);
        builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
      }
      // Note: the reads clauses are not checked for well-formedness (is that sound?), because it used to
      // be that the syntax was not rich enough for programmers to specify reads clauses and always being
      // absolutely well-defined.
      // check well-formedness of the decreases clauses
      foreach (Expression p in f.Decreases) {
        // Note, in this well-formedness check, function is passed in as null.  This will cause there to be
        // no reads checks or decreases checks.  This seems like a good idea, and I hope it is also sound.
        CheckWellformed(p, null, Position.Positive, locals, builder, etran);
      }
      // check well-formedness of the body
      if (f.Body != null) {
        DefineFrame(f.tok, f.Reads, builder, locals);
        CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);
      }

      Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name,
        typeParams,
        Bpl.Formal.StripWhereClauses(proc.InParams),
        Bpl.Formal.StripWhereClauses(proc.OutParams),
        locals, builder.Collect(f.tok));
      sink.TopLevelDeclarations.Add(impl);
    }
    
    Bpl.Expr! IsTotal(Expression! expr, ExpressionTranslator! etran)
      requires predef != null;
    {
      if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
        return Bpl.Expr.True;
      } else if (expr is DisplayExpression) {
        DisplayExpression e = (DisplayExpression)expr;
        return IsTotal(e.Elements, etran);
      } else if (expr is FieldSelectExpr) {
        FieldSelectExpr e = (FieldSelectExpr)expr;
        if (e.Obj is ThisExpr) {
          return Bpl.Expr.True;
        } else {
          return Bpl.Expr.And(IsTotal(e.Obj, etran), Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));
        }
      } else if (expr is SeqSelectExpr) {
        SeqSelectExpr e = (SeqSelectExpr)expr;
        bool isSequence = e.Seq.Type is SeqType;
        Bpl.Expr total = IsTotal(e.Seq, etran);
        Bpl.Expr seq = etran.TrExpr(e.Seq);
        Bpl.Expr e0 = null;
        if (e.E0 != null) {
          e0 = etran.TrExpr(e.E0);
          total = BplAnd(total, IsTotal(e.E0, etran));
          total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));
        }
        if (e.E1 != null) {
          total = BplAnd(total, IsTotal(e.E1, etran));
          total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));
        }
        return total;
      } else if (expr is SeqUpdateExpr) {
        SeqUpdateExpr e = (SeqUpdateExpr)expr;
        Bpl.Expr total = IsTotal(e.Seq, etran);
        Bpl.Expr seq = etran.TrExpr(e.Seq);
        Bpl.Expr index = etran.TrExpr(e.Index);
        total = BplAnd(total, IsTotal(e.Index, etran));
        total = BplAnd(total, InSeqRange(expr.tok, index, seq, true, null, false));
        total = BplAnd(total, IsTotal(e.Value, etran));
        return total;
      } else if (expr is FunctionCallExpr) {
        FunctionCallExpr e = (FunctionCallExpr)expr;
        assert e.Function != null;  // follows from the fact that expr has been successfully resolved
        // check well-formedness of receiver
        Bpl.Expr r = IsTotal(e.Receiver, etran);
        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
          r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null));
        }
        // check well-formedness of the other parameters
        r = BplAnd(r, IsTotal(e.Args, etran));
        // create a substitution map from each formal parameter to the corresponding actual parameter
        Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
        for (int i = 0; i < e.Function.Formals.Count; i++) {
          substMap.Add(e.Function.Formals[i], e.Args[i]);
        }
        // check that the preconditions for the call hold
        foreach (Expression p in e.Function.Req) {
          Expression precond = Substitute(p, e.Receiver, substMap);
          r = BplAnd(r, etran.TrExpr(precond));
        }
        return r;
      } else if (expr is DatatypeValue) {
        DatatypeValue dtv = (DatatypeValue)expr;
        return IsTotal(dtv.Arguments, etran);
      } else if (expr is OldExpr) {
        OldExpr e = (OldExpr)expr;
        return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran));
      } else if (expr is FreshExpr) {
        FreshExpr e = (FreshExpr)expr;
        return IsTotal(e.E, etran);
      } else if (expr is UnaryExpr) {
        UnaryExpr e = (UnaryExpr)expr;
        Bpl.Expr t = IsTotal(e.E, etran);
        if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
          return Bpl.Expr.And(t, Bpl.Expr.Neq(etran.TrExpr(e.E), predef.Null));
        }
        return t;
      } else if (expr is BinaryExpr) {
        BinaryExpr e = (BinaryExpr)expr;
        Bpl.Expr t0 = IsTotal(e.E0, etran);
        Bpl.Expr t1 = IsTotal(e.E1, etran);
        Bpl.Expr z = null;
        switch (e.ResolvedOp) {
          case BinaryExpr.ResolvedOpcode.And:
          case BinaryExpr.ResolvedOpcode.Imp:
            t1 = Bpl.Expr.Imp(etran.TrExpr(e.E0), t1);
            break;
          case BinaryExpr.ResolvedOpcode.Or:
            t1 = Bpl.Expr.Imp(Bpl.Expr.Not(etran.TrExpr(e.E0)), t1);
            break;
          case BinaryExpr.ResolvedOpcode.Div:
          case BinaryExpr.ResolvedOpcode.Mod:
            z = Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0));
            break;
          default:
            break;
        }
        Bpl.Expr r = BplAnd(t0, t1);
        return z == null ? r : BplAnd(r, z);
      } else if (expr is QuantifierExpr) {
        QuantifierExpr e = (QuantifierExpr)expr;
        Bpl.Expr total = IsTotal(e.Body, etran);
        if (total != Bpl.Expr.True) {
          Bpl.VariableSeq bvars = new Bpl.VariableSeq();
          foreach (BoundVar bv in e.BoundVars) {
            bvars.Add(new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, TrType(bv.Type))));
          }
          total = new Bpl.ForallExpr(expr.tok, bvars, total);
        }
        return total;
      } else if (expr is ITEExpr) {
        ITEExpr e = (ITEExpr)expr;
        Bpl.Expr total = IsTotal(e.Test, etran);
        Bpl.Expr test = etran.TrExpr(e.Test);
        total = BplAnd(total, Bpl.Expr.Imp(test, IsTotal(e.Thn, etran)));
        total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), IsTotal(e.Els, etran)));
        return total;
      } else {
        assert false;  // unexpected expression
      }
    }
    
    Bpl.Expr! IsTotal(List<Expression!>! exprs, ExpressionTranslator! etran) {
      Bpl.Expr total = Bpl.Expr.True;
      foreach (Expression e in exprs) {
        total = BplAnd(total, IsTotal(e, etran));
      }
      return total;
    }
    
    Bpl.Expr! BplAnd(Bpl.Expr! a, Bpl.Expr! b) {
      if (a == Bpl.Expr.True) {
        return b;
      } else if (b == Bpl.Expr.True) {
        return a;
      } else {
        return Bpl.Expr.And(a, b);
      }
    }
    
    enum Position { Positive, Negative, Neither }
    Position Negate(Position pos) {
      switch (pos) {
        case Position.Positive:  return Position.Negative;
        case Position.Negative:  return Position.Positive;
        case Position.Neither:  return Position.Neither;
        default:  assert false;  // unexpected Position
      }
    }

    void CheckNonNull(IToken! tok, Expression! e, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
      requires predef != null;
    {
      if (e is ThisExpr) {
        // already known to be non-null
      } else {
        builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), "target object may be null"));
      }
    }

    void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.VariableSeq! locals, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
      requires predef != null;
    {
      if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
        // always allowed
      } else if (expr is DisplayExpression) {
        DisplayExpression e = (DisplayExpression)expr;
        foreach (Expression el in e.Elements) {
          CheckWellformed(el, func, Position.Neither, locals, builder, etran);
        }
      } else if (expr is FieldSelectExpr) {
        FieldSelectExpr e = (FieldSelectExpr)expr;
        CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);
        CheckNonNull(expr.tok, e.Obj, builder, etran);
        if (func != null) {
          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field"));
        }
      } else if (expr is SeqSelectExpr) {
        SeqSelectExpr e = (SeqSelectExpr)expr;
        bool isSequence = e.Seq.Type is SeqType;
        CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
        Bpl.Expr seq = etran.TrExpr(e.Seq);
        Bpl.Expr e0 = null;
        if (e.E0 != null) {
          e0 = etran.TrExpr(e.E0);
          CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);
          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range"));
        }
        if (e.E1 != null) {
          CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);
          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array")));
        }
        if (func != null && ((!)e.Seq.Type).IsArrayType) {
          assert e.E0 != null;
          Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element"));
        }
      } else if (expr is SeqUpdateExpr) {
        SeqUpdateExpr e = (SeqUpdateExpr)expr;
        CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
        Bpl.Expr seq = etran.TrExpr(e.Seq);
        Bpl.Expr index = etran.TrExpr(e.Index);
        CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);
        builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range"));
        CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);
      } else if (expr is FunctionCallExpr) {
        FunctionCallExpr e = (FunctionCallExpr)expr;
        assert e.Function != null;  // follows from the fact that expr has been successfully resolved
        // check well-formedness of receiver
        CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran);
        if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
          CheckNonNull(expr.tok, e.Receiver, builder, etran);
        }
        // check well-formedness of the other parameters
        foreach (Expression arg in e.Args) {
          CheckWellformed(arg, func, Position.Neither, locals, builder, etran);
        }
        // create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
        Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
        for (int i = 0; i < e.Function.Formals.Count; i++) {
          Formal p = e.Function.Formals[i];
          VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);
          local.type = local.OptionalType;  // resolve local here
          IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
          ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here
          substMap.Add(p, ie);
          locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
          Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?
          Expression ee = e.Args[i];
          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), (!)ee.Type, p.Type));
          builder.Add(cmd);
        }
        // check that the preconditions for the call hold
        foreach (Expression p in e.Function.Req) {
          Expression precond = Substitute(p, e.Receiver, substMap);
          builder.Add(Assert(expr.tok, etran.TrExpr(precond), "possible violation of function precondition"));
        }
        if (func != null) {
          // check that the callee reads only what the caller is already allowed to read
          CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function");
  
          // finally, check that the decreases measure goes down
          ModuleDecl module = ((!)e.Function.EnclosingClass).Module;
          if (module == ((!)func.EnclosingClass).Module) {
            if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(func)) {
              List<Expression!> contextDecreases = func.Decreases;
              if (contextDecreases.Count == 0) {
                contextDecreases = new List<Expression!>();
                contextDecreases.Add(FrameToObjectSet(func.Reads));  // use its reads clause instead
              }
              List<Expression!> calleeDecreases = e.Function.Decreases;
              if (calleeDecreases.Count == 0) {
                calleeDecreases = new List<Expression!>();
                calleeDecreases.Add(FrameToObjectSet(e.Function.Reads));  // use its reads clause instead
              }
              CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
            }
          }
        }
      } else if (expr is DatatypeValue) {
        DatatypeValue dtv = (DatatypeValue)expr;
        foreach (Expression arg in dtv.Arguments) {
          CheckWellformed(arg, func, Position.Neither, locals, builder, etran);
        }
      } else if (expr is OldExpr) {
        OldExpr e = (OldExpr)expr;
        CheckWellformed(e.E, func, pos, locals, builder, etran.Old);
      } else if (expr is FreshExpr) {
        FreshExpr e = (FreshExpr)expr;
        CheckWellformed(e.E, func, pos, locals, builder, etran);
      } else if (expr is UnaryExpr) {
        UnaryExpr e = (UnaryExpr)expr;
        CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);
        if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
          CheckNonNull(expr.tok, e.E, builder, etran);
        }
      } else if (expr is BinaryExpr) {
        BinaryExpr e = (BinaryExpr)expr;
        CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);
        switch (e.ResolvedOp) {
          case BinaryExpr.ResolvedOpcode.And:
          case BinaryExpr.ResolvedOpcode.Imp:
            {
              Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
              CheckWellformed(e.E1, func, pos, locals, b, etran);
              builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.E0), b.Collect(expr.tok), null, null));
            }
            break;
          case BinaryExpr.ResolvedOpcode.Or:
            {
              Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
              CheckWellformed(e.E1, func, pos, locals, b, etran);
              builder.Add(new Bpl.IfCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(expr.tok), null, null));
            }
            break;
          case BinaryExpr.ResolvedOpcode.Div:
          case BinaryExpr.ResolvedOpcode.Mod:
            CheckWellformed(e.E1, func, pos, locals, builder, etran);
            builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero"));
            break;
          default:
            CheckWellformed(e.E1, func, pos, locals, builder, etran);
            break;
        }

      } else if (expr is QuantifierExpr) {
        QuantifierExpr e = (QuantifierExpr)expr;
        Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
        foreach (BoundVar bv in e.BoundVars) {
          VarDecl local = new VarDecl(bv.tok, bv.Name, bv.Type, bv.IsGhost, null);
          local.type = local.OptionalType;  // resolve local here
          IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
          ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here
          substMap.Add(bv, ie);
          locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
        }
        Expression body = Substitute(e.Body, null, substMap);
        CheckWellformed(body, func, pos, locals, builder, etran);

      } else if (expr is ITEExpr) {
        ITEExpr e = (ITEExpr)expr;
        CheckWellformed(e.Test, func, pos, locals, builder, etran);
        Bpl.StmtListBuilder bThen = new Bpl.StmtListBuilder();
        Bpl.StmtListBuilder bElse = new Bpl.StmtListBuilder();
        CheckWellformed(e.Thn, func, pos, locals, bThen, etran);
        CheckWellformed(e.Els, func, pos, locals, bElse, etran);
        builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));
      
      } else if (expr is MatchExpr) {
        MatchExpr me = (MatchExpr)expr;
        CheckWellformed(me.Source, func, pos, locals, builder, etran);
        Bpl.Expr src = etran.TrExpr(me.Source);
        foreach (MatchCaseExpr mc in me.Cases) {
          assert mc.Ctor != null;  // follows from the fact that mc has been successfully resolved
          Bpl.ExprSeq args = new Bpl.ExprSeq();
          for (int i = 0; i < mc.Arguments.Count; i++) {
            BoundVar p = mc.Arguments[i];
            Bpl.Variable local = new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
            locals.Add(local);
            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);
            ie.Var = p;  ie.Type = ie.Var.Type;  // resolve it here

            Type t = mc.Ctor.Formals[i].Type;
            args.Add(etran.CondApplyBox(expr.tok, new Bpl.IdentifierExpr(p.tok, local), (!)p.Type, t));
          }
          Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);
          Bpl.Expr ct = new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);

          // generate:  if (src == ctor(args)) { mc.Body is well-formed }
          Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
          CheckWellformed(mc.Body, func, pos, locals, b, etran);
          builder.Add(new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), null, null));
        }
        
      } else {
        assert false;  // unexpected expression
      }
    }
    
    Expression! FrameToObjectSet(List<FrameExpression!>! fexprs) {
      List<Expression!> sets = new List<Expression!>();
      List<Expression!> singletons = null;
      foreach (FrameExpression fe in fexprs) {
        if (fe.E is WildcardExpr) {
          // drop wildcards altogether
        } else {
          Expression e = fe.E;  // keep only fe.E, drop any fe.Field designation
          assert e.Type != null;  // should have been resolved already
          if (e.Type.IsRefType) {
            // e represents a singleton set
            if (singletons == null) {
              singletons = new List<Expression!>();
            }
            singletons.Add(e);
          } else {
            // e is already a set
            assert e.Type is SetType;
            sets.Add(e);
          }
        }
      }
      if (singletons != null) {
        Expression display = new SetDisplayExpr(singletons[0].tok, singletons);
        display.Type = new SetType(new ObjectType());  // resolve here
        sets.Add(display);
      }
      if (sets.Count == 0) {
        Expression emptyset = new SetDisplayExpr(Token.NoToken, new List<Expression!>());
        emptyset.Type = new SetType(new ObjectType());  // resolve here
        return emptyset;
      } else {
        Expression s = sets[0];
        for (int i = 1; i < sets.Count; i++) {
          BinaryExpr union = new BinaryExpr(s.tok, BinaryExpr.Opcode.Add, s, sets[i]);
          union.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here
          union.Type = new SetType(new ObjectType());  // resolve here
          s = union;
        }
        return s;
      }
    }
    
    Bpl.Constant! GetClass(TopLevelDecl! cl)
      requires predef != null;
    {
      Bpl.Constant cc;
      if (classes.TryGetValue(cl, out cc)) {
        assert cc != null;
      } else {
        cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.Name, predef.ClassNameType), true);
        classes.Add(cl, cc);
      }
      return cc;
    }
    
    Bpl.Expr GetTypeExpr(IToken! tok, Type! type)
      requires predef != null;
    {
      while (true) {
        TypeProxy tp = type as TypeProxy;
        if (tp == null) {
          break;
        } else if (tp.T == null) {
          // unresolved proxy
          // TODO: what to do here?
          return null;
        } else {
          type = tp.T;
        }
      }

      if (type is BoolType) {
        return new Bpl.IdentifierExpr(tok, "class.bool", predef.ClassNameType);
      } else if (type is IntType) {
        return new Bpl.IdentifierExpr(tok, "class.int", predef.ClassNameType);
      } else if (type is ObjectType) {
        return new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType);
      } else if (type is CollectionType) {
        CollectionType ct = (CollectionType)type;
        Bpl.Expr a = GetTypeExpr(tok, ct.Arg);
        if (a == null) {
         return null;
        }
        Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType);
        return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
      } else {
        UserDefinedType ct = (UserDefinedType)type;
        if (ct.ResolvedClass == null) {
         return null;  // TODO: what to do here?
        }
        Bpl.Expr t = new Bpl.IdentifierExpr(tok, GetClass(ct.ResolvedClass));
        foreach (Type arg in ct.TypeArgs) {
          Bpl.Expr a = GetTypeExpr(tok, arg);
          if (a == null) {
            return null;
          }
          t = FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
        }
        return t;
      }
    }
    
    Bpl.Constant! GetField(Field! f)
      requires sink != null && predef != null;
    {
      Bpl.Constant fc;
      if (fields.TryGetValue(f, out fc)) {
        assert fc != null;
      } else {
        // const unique f: Field ty;
        Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
        fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);
        fields.Add(f, fc);
        // axiom FCat(f) == $NamedField && DeclType(f) == C;
        Bpl.Expr fcat = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FCat, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, "$NamedField", predef.FieldCategoryType));
        Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass)));
        Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fcat, declType));
        sink.TopLevelDeclarations.Add(ax);
      }
      return fc;
    }
    
    Bpl.Expr! GetField(FieldSelectExpr! fse)
      requires fse.Field != null;
    {
      return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
    }

    /// <summary>
    /// This method is expected to be called just once for each function in the program.
    /// </summary>    
    void AddFunction(Function! f)
      requires predef != null && sink != null;
    {
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
      Bpl.VariableSeq args = new Bpl.VariableSeq();
      args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true));
      if (!f.IsStatic) {
        args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));
      }
      foreach (Formal p in f.Formals) {
        args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true));
      }
      Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);
      Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
      sink.TopLevelDeclarations.Add(func);
      
      if (f.IsRecursive && !f.IsUnlimited) {
        Bpl.Function limitedF = new Bpl.Function(f.tok, f.FullName + "#limited", args, res);
        sink.TopLevelDeclarations.Add(limitedF);
      }
    }
    
    /// <summary>
    /// This method is expected to be called just twice for each procedure in the program (once with
    /// wellformednessProc set to true, once with wellformednessProc set to false).
    /// </summary>    
    Bpl.Procedure! AddMethod(Method! m, bool wellformednessProc)
      requires predef != null && sink != null;
      requires m.EnclosingClass != null;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
      
      Bpl.VariableSeq inParams = new Bpl.VariableSeq();
      Bpl.VariableSeq outParams = new Bpl.VariableSeq();
      if (!m.IsStatic) {
        Bpl.Expr wh = Bpl.Expr.And(
          Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),
          etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, m.EnclosingClass)));
        Bpl.Formal thVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, "this", predef.RefType, wh), true);
        inParams.Add(thVar);
      }
      foreach (Formal p in m.Ins) {
        Bpl.Type varType = TrType(p.Type);
        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
        inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
      }
      foreach (Formal p in m.Outs) {
        Bpl.Type varType = TrType(p.Type);
        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
        outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
      }
      
      Bpl.RequiresSeq req = new Bpl.RequiresSeq();
      Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();
      Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();
      // free requires mh == ModuleContextHeight && InMethodContext;
      Bpl.Expr context = Bpl.Expr.And(
        Bpl.Expr.Eq(Bpl.Expr.Literal(m.EnclosingClass.Module.Height), etran.ModuleContextHeight()),
        etran.InMethodContext());
      req.Add(Requires(m.tok, true, context, null, null));
      mod.Add(etran.HeapExpr);
      mod.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int));
      
      if (!wellformednessProc) {
        string comment = "user-defined preconditions";
        foreach (MaybeFreeExpression p in m.Req) {
          if (p.IsFree) {
            req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
          } else {
            List<Expression!>! definitions, pieces;
            if (!SplitExpr(p.E, out definitions, out pieces)) {
              req.Add(Requires(p.E.tok, false, etran.TrExpr(p.E), null, comment));
            } else {
              req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));  // add the entire condition as a free precondition
              Bpl.Expr ante = Bpl.Expr.True;
              foreach (Expression d in definitions) {
                Bpl.Expr trD = etran.TrExpr(d);
                req.Add(Requires(d.tok, true, trD, null, null));
                ante = Bpl.Expr.And(ante, trD);
              }
              foreach (Expression se in pieces) {
                req.Add(Requires(se.tok, false, Bpl.Expr.Imp(ante, etran.TrExpr(se)), null, null));  // TODO: it would be fine to have these use {:subsumption 0}
              }
            }
          }
          comment = null;
        }
        comment = "user-defined postconditions";
        foreach (MaybeFreeExpression p in m.Ens) {
          if (p.IsFree) {
            ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
          } else {
            List<Expression!>! definitions, pieces;
            if (!SplitExpr(p.E, out definitions, out pieces)) {
              ens.Add(Ensures(p.E.tok, false, etran.TrExpr(p.E), null, comment));
            } else {
              ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));  // add the entire condition as a free postcondition
              Bpl.Expr ante = Bpl.Expr.True;
              foreach (Expression d in definitions) {
                Bpl.Expr trD = etran.TrExpr(d);
                ens.Add(Ensures(d.tok, true, trD, null, null));
                ante = Bpl.Expr.And(ante, trD);
              }
              foreach (Expression se in pieces) {
                ens.Add(Ensures(se.tok, false, Bpl.Expr.Imp(ante, etran.TrExpr(se)), null, null));  // TODO: it would be fine to have these use {:subsumption 0}
              }
            }
          }
          comment = null;
        }
        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {
          ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));
        }
      }

      // CEV information
      // free requires #cev_pc == 0;
      req.Add(Requires(m.tok, true, Bpl.Expr.Eq(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(0)), null, "CEV information"));
      // free requires #cev_init(0);
      req.Add(Requires(m.tok, true, FunctionCall(m.tok, BuiltinFunction.CevInit, null, Bpl.Expr.Literal(0)), null, null));
      // free requires #cev_var_intro(0, cev_implicit, #loc.$Heap, $Heap, 0);
      req.Add(Requires(m.tok, true, FunctionCall(m.tok, BuiltinFunction.CevVarIntro, null,
        Bpl.Expr.Literal(0),
        new Bpl.IdentifierExpr(m.tok, "cev_implicit", predef.CevVariableKind),
        CevVariable(m.tok, predef.HeapVarName),
        etran.HeapExpr,
        Bpl.Expr.Literal(0)), null, null));
      // free requires #cev_save_position(0) == #tok.Tok;
      req.Add(Requires(m.tok, true, Bpl.Expr.Eq(FunctionCall(m.tok, BuiltinFunction.CevProgramLocation, null, Bpl.Expr.Literal(0)), CevLocation(m.tok)), null, null));
      // free ensures old(#cev_pc) < #cev_pc;
      ens.Add(Ensures(m.tok, true, Bpl.Expr.Lt(new Bpl.OldExpr(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int)), Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int)), null, "CEV information"));

      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
      string name = wellformednessProc ? "CheckWellformed$$" + m.FullName : m.FullName;
      Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);
      sink.TopLevelDeclarations.Add(proc);
      return proc;
    }
    
    class BoilerplateTriple {  // a triple that is now a quintuple
      public readonly IToken! tok;
      public readonly bool IsFree;
      public readonly Bpl.Expr! Expr;
      public readonly string ErrorMessage;
      invariant IsFree || ErrorMessage != null;
      public readonly string Comment;
      public BoilerplateTriple(IToken! tok, bool isFree, Bpl.Expr! expr, string errorMessage, string comment)
        requires isFree || errorMessage != null;
      {
        this.tok = tok;
        IsFree = isFree;
        Expr = expr;
        ErrorMessage = errorMessage;
        Comment = comment;
      }
    }
    
    /// <summary>
    /// There are 3 states of interest when generating two-state boilerplate:
    ///  S0. the beginning of the method, which is where the modifies clause is interpreted
    ///  S1. the pre-state of the two-state interval
    ///  S2. the post-state of the two-state interval
    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
    /// </summary>
    List<BoilerplateTriple!>! GetTwoStateBoilerplate(IToken! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
    {
      List<BoilerplateTriple!> boilerplate = new List<BoilerplateTriple!>();
      
      // the frame condition, which is free since it is checked with every heap update and call
      boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));

      // HeapSucc(S1, S2)
      Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
      boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));
      
      return boilerplate;
    }
    
    /// <summary>
    /// There are 3 states of interest when generating a freame condition:
    ///  S0. the beginning of the method, which is where the modifies clause is interpreted
    ///  S1. the pre-state of the two-state interval
    ///  S2. the post-state of the two-state interval
    /// This method assumes that etranPre denotes S1, etran denotes S2, and that etran.Old denotes S0.
    /// </summary>
    Bpl.Expr! FrameCondition(IToken! tok, List<FrameExpression!>! modifiesClause, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
      requires predef != null;
    {
      // generate:
      //  (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }
      //      o != null && old($Heap)[o,alloc] ==>
      //        $Heap[o,f] == PreHeap[o,f] ||
      //        (o,f) in modifiesClause)
      Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");
      Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));
      Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);
      Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));
      Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);
      
      Bpl.Expr heapOF = Bpl.Expr.SelectTok(tok, etran.HeapExpr, o, f);
      Bpl.Expr preHeapOF = Bpl.Expr.SelectTok(tok, etranPre.HeapExpr, o, f);
      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
      Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
      
      consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etran.Old, null, null));
      
      Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
      return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
    }
    
    // ----- Type ---------------------------------------------------------------------------------
    
    Bpl.Type! TrType(Type! type)
      requires predef != null;
    {
      while (true) {
        TypeProxy tp = type as TypeProxy;
        if (tp == null) {
          break;
        } else if (tp.T == null) {
          // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type
          return predef.RefType;
        } else {
          type = tp.T;
        }
      }
      
      if (type is BoolType) {
        return Bpl.Type.Bool;
      } else if (type is IntType) {
        return Bpl.Type.Int;
      } else if (type.IsTypeParameter) {
        return predef.BoxType;
      } else if (type.IsRefType) {
        // object and class types translate to ref
        return predef.RefType;
      } else if (type.IsDatatype) {
        return predef.DatatypeType;
      } else if (type is SetType) {
        return predef.SetType(Token.NoToken, predef.BoxType);
      } else if (type is SeqType) {
        return predef.SeqType(Token.NoToken, predef.BoxType);
      } else {
        assert false;  // unexpected type
      }
    }
    
    Bpl.TypeVariableSeq! TrTypeParamDecls(List<TypeParameter!>! tps)
    {
      Bpl.TypeVariableSeq typeParams = new Bpl.TypeVariableSeq();
      return typeParams;
    }

    // ----- Statement ----------------------------------------------------------------------------
    
    Bpl.AssertCmd! Assert(Bpl.IToken! tok, Bpl.Expr! condition, string! errorMessage)
    {
      Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition);
      cmd.ErrorData = "Error: " + errorMessage;
      return cmd;
    }

    Bpl.AssertCmd! AssertNS(Bpl.IToken! tok, Bpl.Expr! condition, string! errorMessage)
    {
      List<object!> args = new List<object!>();
      args.Add(Bpl.Expr.Literal(0));
      Bpl.QKeyValue kv = new Bpl.QKeyValue(tok, "subsumption", args, null);
      Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, kv);
      cmd.ErrorData = "Error: " + errorMessage;
      return cmd;
    }

    Bpl.Ensures! Ensures(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
    {
      Bpl.Ensures ens = new Bpl.Ensures(tok, free, condition, comment);
      if (errorMessage != null) {
        ens.ErrorData = errorMessage;
      }
      return ens;
    }

    Bpl.Requires! Requires(IToken! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
    {
      Bpl.Requires req = new Bpl.Requires(tok, free, condition, comment);
      if (errorMessage != null) {
        req.ErrorData = errorMessage;
      }
      return req;
    }

    Bpl.StmtList! TrStmt2StmtList(Statement! block, Bpl.VariableSeq! locals, ExpressionTranslator! etran)
      requires currentMethod != null && predef != null;
    {
      return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
    }
    
    Bpl.StmtList! TrStmt2StmtList(Bpl.StmtListBuilder! builder, Statement! block, Bpl.VariableSeq! locals, ExpressionTranslator! etran)
      requires currentMethod != null && predef != null;
    {
      TrStmt(block, builder, locals, etran);
      return builder.Collect(block.Tok);  // TODO: would be nice to have an end-curly location for "block"
    }
    
    void TrStmt(Statement! stmt, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals, ExpressionTranslator! etran)
      requires currentMethod != null && predef != null;
    {
      if (stmt is AssertStmt) {
        AddComment(builder, stmt, "assert statement");
        AssertStmt s = (AssertStmt)stmt;
        builder.Add(AssertNS(s.Expr.tok, IsTotal(s.Expr, etran), "assert condition must be well defined"));  // totality check
        List<Expression!>! definitions, pieces;
        if (!SplitExpr(s.Expr, out definitions, out pieces)) {
          builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));
        } else {
          foreach (Expression p in definitions) {
            builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
          }
          foreach (Expression p in pieces) {
            builder.Add(AssertNS(p.tok, etran.TrExpr(p), "assertion violation"));
          }
          builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
        }
      } else if (stmt is AssumeStmt) {
        AddComment(builder, stmt, "assume statement");
        AssumeStmt s = (AssumeStmt)stmt;
        builder.Add(AssertNS(stmt.Tok, IsTotal(s.Expr, etran), "assume condition must be well defined"));  // totality check
        builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
      } else if (stmt is UseStmt) {
        AddComment(builder, stmt, "use statement");
        UseStmt s = (UseStmt)stmt;
        // Skip the totality check.  This makes the 'use' statement easier to use and it has no executable analog anyhow
        // builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined"));  // totality check
        builder.Add(new Bpl.AssumeCmd(stmt.Tok, (s.EvalInOld ? etran.Old : etran).TrUseExpr(s.FunctionCallExpr)));
      } else if (stmt is PrintStmt) {
        AddComment(builder, stmt, "print statement");
        PrintStmt s = (PrintStmt)stmt;
        foreach (Attributes.Argument arg in s.Args) {
          if (arg.E != null) {
            builder.Add(AssertNS(stmt.Tok, IsTotal(arg.E, etran), "print expression must be well defined"));  // totality check
          }
        }
        
      } else if (stmt is LabelStmt) {
        AddComment(builder, stmt, "label statement");  // TODO: ouch, comments probably mess up what the label labels in the Boogie program
        builder.AddLabelCmd(((LabelStmt)stmt).Label);
      } else if (stmt is BreakStmt) {
        AddComment(builder, stmt, "break statement");
        builder.Add(new Bpl.BreakCmd(stmt.Tok, ((BreakStmt)stmt).TargetLabel));  // TODO: handle name clashes of labels
      } else if (stmt is ReturnStmt) {
        AddComment(builder, stmt, "return statement");
        builder.Add(new Bpl.ReturnCmd(stmt.Tok));
      } else if (stmt is AssignStmt) {
        AddComment(builder, stmt, "assignment statement");
        AssignStmt s = (AssignStmt)stmt;
        TrAssignment(stmt.Tok, s.Lhs, s.Rhs, builder, locals, etran);
        if (s.Lhs is IdentifierExpr) {
          Bpl.IdentifierExpr v = etran.TrVar(stmt.Tok, (!)((IdentifierExpr)s.Lhs).Var);
          builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
            new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, v.Name), v),
            new Bpl.IdentifierExprSeq()));
        } else if (s.Lhs is SeqSelectExpr) {
          // TODO: CEV
        } else {
          builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
            new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
            new Bpl.IdentifierExprSeq()));
        }
      } else if (stmt is VarDecl) {
        AddComment(builder, stmt, "var-declaration statement");
        VarDecl s = (VarDecl)stmt;
        Bpl.Type varType = TrType(s.Type);
        Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType), s.Type, etran);
        Bpl.Expr cevWh = FunctionCall(stmt.Tok, BuiltinFunction.CevVarUpdate, null,
          Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int),
          new Bpl.IdentifierExpr(stmt.Tok, "cev_local", predef.CevVariableKind),
          CevVariable(stmt.Tok, s.UniqueName),
          new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType));
        wh = wh == null ? cevWh : Bpl.Expr.And(wh, cevWh);
        Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.UniqueName, varType, wh));
        locals.Add(var);
        if (s.Rhs != null) {
          IdentifierExpr ide = new IdentifierExpr(stmt.Tok, var.Name);  // allocate an expression for the assignment LHS...
          ide.Var = s;  ide.Type = s.Type;  // ... and resolve it right here
          TrAssignment(stmt.Tok, ide, s.Rhs, builder, locals, etran);
        }
        builder.Add(new Bpl.CallCmd(stmt.Tok, "CevVarIntro",
          new Bpl.ExprSeq(
            CevLocation(stmt.Tok),
            new Bpl.IdentifierExpr(stmt.Tok, "cev_local", predef.CevVariableKind),
            CevVariable(stmt.Tok, var.Name),
            new Bpl.IdentifierExpr(stmt.Tok, var)),
          new Bpl.IdentifierExprSeq()));
        
      } else if (stmt is CallStmt) {
        CallStmt s = (CallStmt)stmt;
        foreach (VarDecl local in s.NewVars) {
          TrStmt(local, builder, locals, etran);
        }
        AddComment(builder, stmt, "call statement");
        Bpl.ExprSeq ins = new Bpl.ExprSeq();
        assert s.Method != null;  // follows from the fact that stmt has been successfully resolved
        if (!s.Method.IsStatic) {
          ins.Add(etran.TrExpr(s.Receiver));
        }

        // Ideally, the modifies and decreases checks would be done after the precondition check,
        // but Boogie doesn't give us a hook for that.  So, we set up our own local variables here to
        // store the actual parameters.
        // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
        Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
        for (int i = 0; i < s.Method.Ins.Count; i++) {
          Formal p = s.Method.Ins[i];
          VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);
          local.type = local.OptionalType;  // resolve local here
          IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
          ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here
          substMap.Add(p, ie);
          locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
          
          Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?
          Expression actual = s.Args[i];
          builder.Add(Assert(actual.tok, IsTotal(actual, etran), "argument must be well defined"));  // totality check
          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(stmt.Tok, etran.TrExpr(actual), (!)actual.Type, s.Method.Ins[i].Type));
          builder.Add(cmd);
          ins.Add(lhs);
        }
        // Also create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
        Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
        List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);
        for (int i = 0; i < s.Lhs.Count; i++) {
          Expression e = s.Lhs[i];
          if (ExpressionTranslator.ModeledAsBoxType(s.Method.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) {
            // we need an Unbox
            Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));
            otherTmpVarCount++;
            locals.Add(var);
            Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(stmt.Tok, var.Name, predef.BoxType);
            tmpOuts.Add(varIdE);
            outs.Add(varIdE);
          } else {
            tmpOuts.Add(null);
            outs.Add(etran.TrExpr(e));
          }
        }

        // Check modifies clause
        CheckFrameSubset(stmt.Tok, s.Method.Mod, s.Receiver, substMap, etran, builder, "call may violate caller's modifies clause");

        // Check termination
        ModuleDecl module = ((!)s.Method.EnclosingClass).Module;
        if (module == ((!)currentMethod.EnclosingClass).Module) {
          if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
            CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
          }
        }

        // Make the call
        Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs);
        builder.Add(call);
        for (int i = 0; i < s.Lhs.Count; i++) {
          Bpl.IdentifierExpr tmpVarIdE = tmpOuts[i];
          IdentifierExpr e = s.Lhs[i];
          Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e);  // TODO: is this cast always justified?
          if (tmpVarIdE != null) {
            // e := UnBox(tmpVar);
            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(stmt.Tok, lhs, FunctionCall(stmt.Tok, BuiltinFunction.Unbox, TrType((!)e.Type), tmpVarIdE));
            builder.Add(cmd);
          }
          builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHere",
            new Bpl.ExprSeq(CevVariable(stmt.Tok, e.Name), lhs),
            new Bpl.IdentifierExprSeq()));
        }
        builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStep", new Bpl.ExprSeq(CevLocation(stmt.Tok)), new Bpl.IdentifierExprSeq()));
        
      } else if (stmt is BlockStmt) {
        foreach (Statement ss in ((BlockStmt)stmt).Body) {
          TrStmt(ss, builder, locals, etran);
        }
      } else if (stmt is IfStmt) {
        AddComment(builder, stmt, "if statement");
        IfStmt s = (IfStmt)stmt;
        builder.Add(new Bpl.CallCmd(s.Tok, "CevEvent",
          new Bpl.ExprSeq(CevLocation(s.Tok), new Bpl.IdentifierExpr(s.Tok, "conditional_moment", predef.CevEventType)),
          new Bpl.IdentifierExprSeq()));
        Bpl.Expr guard;
        if (s.Guard == null) {
          guard = null;
        } else {
          builder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "if guard must be well defined"));  // totality check
          guard = etran.TrExpr(s.Guard);
        }
        Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
        b.Add(new Bpl.CallCmd(s.Thn.Tok, "CevEvent",
          new Bpl.ExprSeq(CevLocation(s.Thn.Tok), new Bpl.IdentifierExpr(s.Thn.Tok, "took_then_branch", predef.CevEventType)),
          new Bpl.IdentifierExprSeq()));
        Bpl.StmtList thn = TrStmt2StmtList(b, s.Thn, locals, etran);
        Bpl.StmtList els;
        Bpl.IfCmd elsIf = null;
        if (s.Els == null) {
          b = new Bpl.StmtListBuilder();
          b.Add(new Bpl.CallCmd(s.Tok, "CevEvent",
            new Bpl.ExprSeq(CevLocation(s.Tok), new Bpl.IdentifierExpr(s.Tok, "took_else_branch", predef.CevEventType)),
            new Bpl.IdentifierExprSeq()));
          els = b.Collect(s.Tok);
        } else {
          b = new Bpl.StmtListBuilder();
          b.Add(new Bpl.CallCmd(s.Els.Tok, "CevEvent",
            new Bpl.ExprSeq(CevLocation(s.Els.Tok), new Bpl.IdentifierExpr(s.Els.Tok, "took_else_branch", predef.CevEventType)),
            new Bpl.IdentifierExprSeq()));
          els = TrStmt2StmtList(b, s.Els, locals, etran);
          if (els.BigBlocks.Count == 1) {
            Bpl.BigBlock bb = els.BigBlocks[0];
            if (bb.LabelName == null && bb.simpleCmds.Length == 0 && bb.ec is Bpl.IfCmd) {
              elsIf = (Bpl.IfCmd)bb.ec;
              els = null;
            }
          }
        }
        builder.Add(new Bpl.IfCmd(stmt.Tok, guard, thn, elsIf, els));
        
      } else if (stmt is WhileStmt) {
        AddComment(builder, stmt, "while statement");
        WhileStmt s = (WhileStmt)stmt;
        int loopId = loopHeapVarCount;
        loopHeapVarCount++;
        
        // use simple heuristics to create a default decreases clause, if none is given
        List<Expression!> theDecreases = s.Decreases;
        bool inferredDecreases = false;
        if (theDecreases.Count == 0 && s.Guard != null) {
          Expression prefix = null;
          foreach (Expression guardConjunct in Conjuncts(s.Guard)) {
            Expression guess = null;
            BinaryExpr bin = guardConjunct as BinaryExpr;
            if (bin != null) {
              switch (bin.ResolvedOp) {
                case BinaryExpr.ResolvedOpcode.Lt:
                case BinaryExpr.ResolvedOpcode.Le:
                  // for A < B and A <= B, use the decreases B - A
                  guess = CreateIntSub(s.Tok, bin.E1, bin.E0);
                  break;
                case BinaryExpr.ResolvedOpcode.Ge:
                case BinaryExpr.ResolvedOpcode.Gt:
                  // for A >= B and A > B, use the decreases A - B
                  guess = CreateIntSub(s.Tok, bin.E0, bin.E1);
                  break;
                case BinaryExpr.ResolvedOpcode.NeqCommon:
                  if (bin.E0.Type is IntType) {
                    // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)
                    Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1);
                    Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0);
                    Expression zero = CreateIntLiteral(s.Tok, 0);
                    BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB);
                    test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here
                    test.Type = Type.Bool;  // resolve here
                    guess = CreateIntITE(s.Tok, test, AminusB, BminusA);
                  }
                  break;
                default:
                  break;
              }
            }
            if (guess != null) {
              if (prefix != null) {
                // Make the following guess:  if prefix then guess else -1
                Expression negativeOne = CreateIntLiteral(s.Tok, -1);
                guess = CreateIntITE(s.Tok, prefix, guess, negativeOne);
              }
              theDecreases.Add(guess);
              inferredDecreases = true;
              break;  // ignore any further conjuncts
            }
            if (prefix == null) {
              prefix = guardConjunct;
            } else {
              BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct);
              and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here
              and.Type = Type.Bool;  // resolve here
              prefix = and;
            }
          }
        }
        
        Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
        locals.Add(preLoopHeapVar);
        Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(stmt.Tok, preLoopHeapVar);
        ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
        builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, preLoopHeap, etran.HeapExpr));  // TODO: does this screw up labeled breaks for this loop?

        List<Bpl.Expr!> initDecr = null;
        if (!exists{Expression e in theDecreases; e is WildcardExpr}) {
          initDecr = RecordDecreasesValue(theDecreases, builder, locals, etran, "$decr" + loopId + "$init$");
        }

        // the variable w is used to coordinate the definedness checking of the loop invariant
        Bpl.LocalVariable wVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$w" + loopId, Bpl.Type.Bool));
        Bpl.IdentifierExpr w = new Bpl.IdentifierExpr(stmt.Tok, wVar);
        locals.Add(wVar);
        // havoc w;
        builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq(w)));

        // CEV information
        Bpl.LocalVariable preLoopCevPCVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopCevPC" + loopId, Bpl.Type.Int));
        locals.Add(preLoopCevPCVar);
        Bpl.IdentifierExpr preLoopCevPC = new Bpl.IdentifierExpr(stmt.Tok, preLoopCevPCVar);
        // call preLoopCevPC := CevPreLoop(loc);
        builder.Add(new Bpl.CallCmd(stmt.Tok, "CevPreLoop",
          new Bpl.ExprSeq(CevLocation(stmt.Tok)),
          new Bpl.IdentifierExprSeq(preLoopCevPC)));  // TODO: does this screw up labeled breaks for this loop?
        
        List<Bpl.PredicateCmd!> invariants = new List<Bpl.PredicateCmd!>();
        Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();
        foreach (MaybeFreeExpression loopInv in s.Invariants) {
          invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), (loopInv.IsFree ? "free " : "") + "loop invariant must be well defined"));  // totality check
          invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
          if (loopInv.IsFree) {
            invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
          } else {
            List<Expression!>! definitions, pieces;
            if (!SplitExpr(loopInv.E, out definitions, out pieces)) {
              invariants.Add(Assert(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E)), "loop invariant violation"));
            } else {
              Bpl.Expr ante = w;
              foreach (Expression d in definitions) {
                Bpl.Expr trD = etran.TrExpr(d);
                invariants.Add(new Bpl.AssumeCmd(d.tok, trD));
                ante = Bpl.Expr.And(ante, trD);
              }
              foreach (Expression se in pieces) {
                invariants.Add(Assert(se.tok, Bpl.Expr.Imp(ante, etran.TrExpr(se)), "loop invariant violation"));  // TODO: it would be fine to have this use {:subsumption 0}
              }
              invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
            }
          }
        }
        // check definedness of decreases clause
        foreach (Expression e in theDecreases) {
          invDefinednessBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration"));  // totality check
        }
        // include boilerplate invariants
        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(stmt.Tok, currentMethod, etranPreLoop, etran)) {
          if (tri.IsFree) {
            invariants.Add(new Bpl.AssumeCmd(stmt.Tok, tri.Expr));
          } else {
            assert tri.ErrorMessage != null;  // follows from BoilerplateTriple invariant
            invariants.Add(Assert(stmt.Tok, tri.Expr, tri.ErrorMessage));
          }
        }
        // include a free invariant that says that all completed iterations so far have only decreased the termination metric
        if (initDecr != null) {
          List<IToken!> toks = new List<IToken!>();
          List<Type!> types = new List<Type!>();
          List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
          foreach (Expression e in theDecreases) {
            toks.Add(e.tok);
            types.Add((!)e.Type);
            decrs.Add(etran.TrExpr(e));
          }
          Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, initDecr, etran, null, null, true);
          invariants.Add(new Bpl.AssumeCmd(stmt.Tok, decrCheck));
        }
        
        // CEV information
        invariants.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.Eq(FunctionCall(stmt.Tok, BuiltinFunction.CevProgramLocation, null, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int)), CevLocation(stmt.Tok))));
        invariants.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.Lt(preLoopCevPC, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int))));
        invariants.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.CevControlFlowEvent,
          null,
          Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int),
          new Bpl.IdentifierExpr(stmt.Tok, "loop_register", predef.CevEventType))));
        foreach (Formal p in currentMethod.Outs) {
          Bpl.Expr wh = FunctionCall(stmt.Tok, BuiltinFunction.CevVarUpdate, null,
            Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int),
            new Bpl.IdentifierExpr(stmt.Tok, "cev_local", predef.CevVariableKind),
            CevVariable(stmt.Tok, p.UniqueName),
            etran.TrVar(stmt.Tok, p));
          invariants.Add(new Bpl.AssumeCmd(stmt.Tok, wh));
        }

        Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
        // as the first thing inside the loop, generate:  if (!w) { assert IsTotal(inv); assume false; }
        invDefinednessBuilder.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
        loopBodyBuilder.Add(new Bpl.IfCmd(stmt.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(stmt.Tok), null, null));
        // generate:  assert IsTotal(guard); if (!guard) { break; }
        Bpl.Expr guard;
        if (s.Guard == null) {
          guard = null;
        } else {
          loopBodyBuilder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "loop guard must be well defined"));  // totality check
          Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();
          guardBreak.Add(new Bpl.BreakCmd(s.Guard.tok, null));
          loopBodyBuilder.Add(new Bpl.IfCmd(s.Guard.tok, Bpl.Expr.Not(etran.TrExpr(s.Guard)), guardBreak.Collect(s.Guard.tok), null, null));
          guard = Bpl.Expr.True;
        }
        // CEV information
        loopBodyBuilder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",
          new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
          new Bpl.IdentifierExprSeq()));
        // termination checking
        if (exists{Expression e in theDecreases; e is WildcardExpr}) {
          // omit termination checking for this loop
          TrStmt(s.Body, loopBodyBuilder, locals, etran);
        } else {
          List<Bpl.Expr!> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
          // time for the actual loop body
          TrStmt(s.Body, loopBodyBuilder, locals, etran);
          // check definedness of decreases expressions
          List<IToken!> toks = new List<IToken!>();
          List<Type!> types = new List<Type!>();
          List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
          foreach (Expression e in theDecreases) {
            toks.Add(e.tok);
            types.Add((!)e.Type);
            decrs.Add(etran.TrExpr(e));
          }
          Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false);
          loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));
        }
        Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);

        builder.Add(new Bpl.WhileCmd(stmt.Tok, guard, invariants, body));
        builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",
          new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_exited", predef.CevEventType)),
          new Bpl.IdentifierExprSeq()));

      } else if (stmt is ForeachStmt) {
        AddComment(builder, stmt, "foreach statement");
        ForeachStmt s = (ForeachStmt)stmt;
        // assert/assume (forall o: ref ::  o != null && o in S && Range(o) ==> Expr);
        // assert (forall o: ref :: o != null && o in S && Range(o)  ==> IsTotal(RHS));
        // assert (forall o: ref :: o != null && o in S && Range(o)  ==> $_Frame[o,F]);  // this checks the enclosing modifies clause
        // var oldHeap := $Heap;
        // havoc $Heap;
        // assume $HeapSucc(oldHeap, $Heap);
        // assume (forall<alpha> o: ref, f: Field alpha ::  $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
        // assume (forall o: ref ::  o != null && o in S && Range(o) ==> $Heap[o,F] =  RHS[$Heap := oldHeap]);
        // Note, $Heap[o,alloc] is intentionally omitted from the antecedent of the quantifier in the previous line.  That
        // allocatedness property should hold automatically, because the set/seq quantified is a program expression, which
        // will have been constructed from allocated objects.
        // For sets, "o in S" means just that.  For sequences, "o in S" is:
        //   (exists i :: { Seq#Index(S,i) }  0 <= i && i < Seq#Length(S) && Seq#Index(S,i) == o)

        Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.BoundVar.UniqueName, TrType(s.BoundVar.Type)));
        Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);

        // colection
        builder.Add(Assert(s.Collection.tok, IsTotal(s.Collection, etran), "collection expression must be well defined"));
        Bpl.Expr oInS;
        if (s.Collection.Type is SetType) {
          oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
        } else {
          Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
          Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
          Bpl.Expr S = etran.TrExpr(s.Collection);
          Bpl.Expr range = InSeqRange(stmt.Tok, i, S, true, null, false);
          Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
          Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
          // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
          oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));
        }
        oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
        
        // range
        Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
        builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
        oInS = Bpl.Expr.And(oInS, etran.TrExpr(s.Range));

        // sequence of asserts and assumes and uses
        foreach (PredicateStmt ps in s.BodyPrefix) {
          if (ps is AssertStmt) {
            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
            builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined"));  // totality check
            List<Expression!>! definitions, pieces;
            SplitExpr(ps.Expr, out definitions, out pieces);
            foreach (Expression d in definitions) {
              Bpl.Expr e = etran.TrExpr(d);
              q = new Bpl.ForallExpr(d.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
              builder.Add(new Bpl.AssumeCmd(d.tok, q));
            }
            foreach (Expression se in pieces) {
              Bpl.Expr e = etran.TrExpr(se);
              q = new Bpl.ForallExpr(se.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
              builder.Add(Assert(se.tok, q, "assertion violation"));  // TODO: it would be a fine idea to let this use {:subsumption 0}
            }
          } else if (ps is AssumeStmt) {
            Bpl.Expr eIsTotal = IsTotal(ps.Expr, etran);
            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, eIsTotal));
            builder.Add(AssertNS(ps.Expr.tok, q, "assume condition must be well defined"));  // totality check
          } else {
            assert ps is UseStmt;
            // no totality check (see UseStmt case above)
          }
          Bpl.Expr enchilada;  // the whole enchilada
          if (ps is UseStmt) {
            UseStmt us = (UseStmt)ps;
            enchilada = (us.EvalInOld ? etran.Old : etran).TrUseExpr(us.FunctionCallExpr);
          } else {
            enchilada = etran.TrExpr(ps.Expr);
          }
          Bpl.Expr qEnchilada = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, enchilada));
          builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, qEnchilada));
        }

        // Check RHS of assignment to be well defined
        ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
        if (rhsExpr != null) {
          // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
          Bpl.Expr bbb = Bpl.Expr.Imp(oInS, IsTotal(rhsExpr.Expr, etran));
          Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
          builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined"));  // totality check
        }
              
        // Here comes:  assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
        Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
        Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
        builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));

        // Set up prevHeap
        Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(stmt.Tok, locals);
        builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, prevHeap, etran.HeapExpr));
        builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
        builder.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));

        // Here comes:  assume (forall<alpha> o: ref, f: Field alpha ::  $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
        Bpl.TypeVariable alpha = new Bpl.TypeVariable(stmt.Tok, "alpha");
        Bpl.BoundVariable fVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$f", predef.FieldName(stmt.Tok, alpha)));
        Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
        Bpl.Expr heapOF = Bpl.Expr.SelectTok(stmt.Tok, etran.HeapExpr, o, f);
        Bpl.Expr oldHeapOF = Bpl.Expr.SelectTok(stmt.Tok, prevHeap, o, f);
        body = Bpl.Expr.Or(
          Bpl.Expr.Eq(heapOF, oldHeapOF),
          Bpl.Expr.And(
            Bpl.Expr.Eq(f, GetField((FieldSelectExpr)s.BodyAssign.Lhs)),
            oInS));
        qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
        builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));

        // Here comes:  assume (forall o: ref ::  o != null && o in S && Range(o) ==> $Heap[o,F] =  RHS[$Heap := oldHeap]);
        if (rhsExpr != null) {
          Bpl.Expr heapOField = Bpl.Expr.SelectTok(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
          ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
          body = Bpl.Expr.Imp(oInS, Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(rhsExpr.Expr)));
          qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
          builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
        }
        
        // CEV information
        builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
          new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
          new Bpl.IdentifierExprSeq()));
        
      } else if (stmt is MatchStmt) {
        MatchStmt s = (MatchStmt)stmt;
        builder.Add(Assert(s.Source.tok, IsTotal(s.Source, etran), "match source expression must be well defined"));  // totality check
        Bpl.Expr source = etran.TrExpr(s.Source);
        
        Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
        b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
        Bpl.StmtList els = b.Collect(stmt.Tok);
        Bpl.IfCmd ifCmd = null;
        for (int i = s.Cases.Count; 0 <= --i; ) {
          MatchCaseStmt mc = (MatchCaseStmt)s.Cases[i];
          // havoc all bound variables
          List<Expression!> rArgs = new List<Expression!>();
          Bpl.IdentifierExprSeq havocIds = new Bpl.IdentifierExprSeq();
          foreach (BoundVar arg in mc.Arguments) {
            Bpl.LocalVariable v = new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, arg.UniqueName, TrType(arg.Type)));
            locals.Add(v);
            havocIds.Add(new Bpl.IdentifierExpr(arg.tok, v));
            IdentifierExpr ie = new IdentifierExpr(arg.tok, arg.UniqueName);
            ie.Var = arg;  ie.Type = ie.Var.Type;  // resolve it here
            rArgs.Add(ie);
          }
          if (havocIds.Length != 0) {
            builder.Add(new Bpl.HavocCmd(mc.tok, havocIds));
          }
          assert mc.Ctor != null && mc.Ctor.EnclosingDatatype != null;  // everything has been successfully resolved
          DatatypeValue r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
          r.Ctor = mc.Ctor;  r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type!>()/*this is not right, but it seems like it won't matter here*/);  // resolve it here

          // translate the body into b
          b = new Bpl.StmtListBuilder();
          foreach (Statement ss in mc.Body) {
            TrStmt(ss, b, locals, etran);
          }

          Bpl.Expr guard = Bpl.Expr.Eq(source, etran.TrExpr(r));
          ifCmd = new Bpl.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els);
          els = null;
        }
        assert ifCmd != null;  // follows from the fact that s.Cases.Count != 0.
        builder.Add(ifCmd);

      } else {
        assert false;  // unexpected statement
      }
    }
    
    static Expression! CreateIntLiteral(IToken! tok, int n)
    {
      if (0 <= n) {
        Expression lit = new LiteralExpr(tok, n);
        lit.Type = Type.Int;  // resolve here
        return lit;
      } else {
        return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));
      }
    }
    
    static Expression! CreateIntSub(IToken! tok, Expression! e0, Expression! e1)
      requires e0.Type is IntType && e1.Type is IntType;
    {
      BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here
      s.Type = Type.Int;  // resolve here
      return s;
    }
    
    static Expression! CreateIntITE(IToken! tok, Expression! test, Expression! e0, Expression! e1)
      requires test.Type is BoolType && e0.Type is IntType && e1.Type is IntType;
    {
      ITEExpr ite = new ITEExpr(tok, test, e0, e1);
      ite.Type = Type.Int;  // resolve here
      return ite;
    }
    
    public IEnumerable<Expression!>! Conjuncts(Expression! expr)
      requires expr.Type is BoolType;
    {
      if (expr is BinaryExpr) {
        BinaryExpr bin = (BinaryExpr)expr;
        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
          foreach (Expression e in Conjuncts(bin.E0)) {
            yield return e;
          }
          assert bin != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
          foreach (Expression e in Conjuncts(bin.E1)) {
            yield return e;
          }
          yield break;
        }
      }
      yield return expr;
    }

    List<Bpl.Expr!>! RecordDecreasesValue(List<Expression!>! decreases, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals, ExpressionTranslator! etran, string! varPrefix)
    {
      List<Bpl.Expr!> oldBfs = new List<Bpl.Expr!>();
      int c = 0;
      foreach (Expression e in decreases) {
        Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, varPrefix + c, TrType((!)e.Type)));
        locals.Add(bfVar);
        Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);
        oldBfs.Add(bf);
        // record value of each decreases expression at beginning of the loop iteration
        Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
        builder.Add(cmd);
        
        c++;
      }
      return oldBfs;
    }
        
    void CheckCallTermination(IToken! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
                              Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
                              ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
    {
      int N = min{contextDecreases.Count, calleeDecreases.Count};
      List<IToken!> toks = new List<IToken!>();
      List<Type!> types = new List<Type!>();
      List<Bpl.Expr!> callee = new List<Bpl.Expr!>();
      List<Bpl.Expr!> caller = new List<Bpl.Expr!>();
      for (int i = 0; i < N; i++) {
        Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);
        Expression e1 = contextDecreases[i];
        if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {
          break;
        }
        toks.Add(tok);
        types.Add(e0.Type);
        callee.Add(etran.TrExpr(e0));
        caller.Add(etran.TrExpr(e1));
      }
      Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, etran, builder, "", false);
      builder.Add(Assert(tok, decrExpr, "failure to decrease termination measure"));
    }
    
    /// <summary>
    /// Returns the expression that says whether or not the decreases function has gone down (if !allowNoChange)
    /// or has gone down or stayed the same (if allowNoChange).
    /// ee0 represents the new values and ee1 represents old values.
    /// If builder is non-null, then the check '0 ATMOST decr' is generated to builder.
    /// </summary>
    Bpl.Expr! DecreasesCheck(List<IToken!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
                             ExpressionTranslator! etran,
                             Bpl.StmtListBuilder builder, string suffixMsg, bool allowNoChange)
      requires predef != null;
      requires types.Count == ee0.Count && ee0.Count == ee1.Count;
      requires builder != null <==> suffixMsg != null;
    {
      int N = types.Count;
      
      // compute eq and less for each component of the lexicographic pair
      List<Bpl.Expr!> Eq = new List<Bpl.Expr!>(N);
      List<Bpl.Expr!> Less = new List<Bpl.Expr!>(N);
      for (int i = 0; i < N; i++) {
        Bpl.Expr! less, atmost, eq;
        ComputeLessEq(toks[i], types[i], ee0[i], ee1[i], out less, out atmost, out eq, etran);
        Eq.Add(eq);
        Less.Add(allowNoChange ? atmost : less);
      }
      if (builder != null) {
        // check: 0 <= ee1
        // more precisely, for component k of the lexicographic decreases function, check:
        //   ee0[0] < ee1[0] || ee0[1] < ee1[1] || ... || ee0[k-1] < ee1[k-1] || ee0[k] == ee1[k] || 0 <= ee1[k]
        for (int k = 0; k < N; k++) {
          // we only need to check lower bound for integers--sets, sequences, booleans, references, and datatypes all have natural lower bounds
          Bpl.Expr prefixIsLess = Bpl.Expr.False;
          for (int i = 0; i < k; i++) {
            prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
          }
          if (types[k] is IntType) {
            Bpl.Expr bounded = Bpl.Expr.Le(Bpl.Expr.Literal(0), ee1[k]);
            for (int i = 0; i < k; i++) {
              bounded = Bpl.Expr.Or(bounded, Less[i]);
            }
            string component = N == 1 ? "" : " (component " + k + ")";
            Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by 0" + suffixMsg);
            builder.Add(cmd);
          }
        }
      }
      // check: ee0 < ee1 (or ee0 <= ee1, if allowNoChange)
      Bpl.Expr decrCheck = allowNoChange ? Bpl.Expr.True : Bpl.Expr.False;
      for (int i = N; 0 <= --i; ) {
        Bpl.Expr less = Less[i];
        Bpl.Expr eq = Eq[i];
        if (allowNoChange) {
          // decrCheck = atmost && (eq ==> decrCheck)
          decrCheck = Bpl.Expr.And(less, Bpl.Expr.Imp(eq, decrCheck));
        } else {
          // decrCheck = less || (eq && decrCheck)
          decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
        }
      }
      return decrCheck;
    }

    bool CompatibleDecreasesTypes(Type! t, Type! u) {
      if (t is BoolType) {
        return u is BoolType;
      } else if (t is IntType) {
        return u is IntType;
      } else if (t is SetType) {
        return u is SetType;
      } else if (t is SeqType) {
        return u is SeqType;
      } else if (t.IsDatatype) {
        return u.IsDatatype;
      } else {
        assert t.IsRefType;
        return u.IsRefType;
      }
    }
    
    void ComputeLessEq(IToken! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! atmost, out Bpl.Expr! eq, ExpressionTranslator! etran)
      requires predef != null;
    {
      if (ty is BoolType) {
        eq = Bpl.Expr.Iff(e0, e1);
        less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
        atmost = Bpl.Expr.Imp(e0, e1);
      } else if (ty is IntType) {
        eq = Bpl.Expr.Eq(e0, e1);
        less = Bpl.Expr.Lt(e0, e1);
        atmost = Bpl.Expr.Le(e0, e1);
      } else if (ty is SetType) {
        eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1);
        less = etran.ProperSubset(tok, e0, e1);
        atmost = FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1);
      } else if (ty is SeqType) {
        Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
        Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
        eq = Bpl.Expr.Eq(b0, b1);
        less = Bpl.Expr.Lt(b0, b1);
        atmost = Bpl.Expr.Le(b0, b1);
      } else if (ty.IsDatatype) {
        Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0);
        Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1);
        eq = Bpl.Expr.Eq(b0, b1);
        less = Bpl.Expr.Lt(b0, b1);
        atmost = Bpl.Expr.Le(b0, b1);
        
      } else {
        // reference type
        Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);
        Bpl.Expr b1 = Bpl.Expr.Neq(e1, predef.Null);
        eq = Bpl.Expr.Iff(b0, b1);
        less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
        atmost = Bpl.Expr.Imp(b0, b1);
      }
    }
    
    void AddComment(Bpl.StmtListBuilder! builder, Statement! stmt, string! comment) {
      builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
    }
    
    Bpl.Expr GetWhereClause(IToken! tok, Bpl.Expr! x, Type! type, ExpressionTranslator! etran)
      requires predef != null;
    {
      if (type is TypeProxy) {
        // unresolved proxy
        assert ((TypeProxy)type).T == null;
        // omit where clause (in other places, unresolved proxies are treated as a reference type; we could do that here too, but
        // we might as well leave out the where clause altogether)
        return null;
      } else if (type is BoolType || type is IntType) {
        return null;
      } else if (type is SetType) {
        SetType st = (SetType)type;
        if (st.Arg.IsRefType) {
          // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t) == null || $Heap[Unbox(t),alloc])
          Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t", predef.BoxType));
          Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
          Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t);
          Bpl.Expr unboxT = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, t);

          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
          
          Bpl.Expr goodRef = etran.GoodRef(tok, unboxT, st.Arg);
          Bpl.Expr body = Bpl.Expr.Imp(xSubT, Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));
          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, body);
        } else {
          // TODO:  should also handle sets of sets, etc.
          return null;
        }
        
      } else if (type is SeqType) {
        SeqType st = (SeqType)type;
        if (st.Arg.IsRefType) {
          // (forall i: int :: { Seq#Index(x,i) }
          //      0 <= i && i < Seq#Length(x) ==> Unbox(Seq#Index(x,i)) == null || $Heap[Unbox(Seq#Index(x,i)), alloc])
          Bpl.BoundVariable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
          Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
          Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);
          Bpl.Expr unbox = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, xSubI);

          Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);

          Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));

          Bpl.Expr goodRef = etran.GoodRef(tok, unbox, st.Arg);
          Bpl.Expr body = Bpl.Expr.Imp(range, Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));
          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, body);
        } else {
          // TODO: should also handle sequences or sequences, etc.
          return null;
        }

      } else if (type.IsRefType) {
        // reference type:
        // x == null || $Heap[x,alloc]
        return Bpl.Expr.Or(Bpl.Expr.Eq(x, predef.Null), etran.GoodRef(tok, x, type));
      } else {
        // type parameter
        return null;
      }
    }
    
    void TrAssignment(IToken! tok, Expression! lhs, AssignmentRhs! rhs, Bpl.StmtListBuilder! builder, Bpl.VariableSeq! locals,
                      ExpressionTranslator! etran)
      requires predef != null;
    {
      if (rhs is ExprRhs) {
        builder.Add(Assert(tok, IsTotal(lhs, etran), "LHS expression must be well defined"));  // totality check
        builder.Add(Assert(tok, IsTotal(((ExprRhs)rhs).Expr, etran), "RHS expression must be well defined"));  // totality check
        Bpl.Expr bRhs = etran.TrExpr(((ExprRhs)rhs).Expr);
        if (lhs is IdentifierExpr) {
          Bpl.IdentifierExpr bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?
          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
          builder.Add(cmd);
        } else if (lhs is FieldSelectExpr) {
          FieldSelectExpr fse = (FieldSelectExpr)lhs;
          assert fse.Field != null;
          // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj];
          builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(fse.Obj), GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));
          
          Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr;  // TODO: is this cast always justified?
          bRhs = etran.CondApplyBox(tok, bRhs, (!)((ExprRhs)rhs).Expr.Type, fse.Field.Type);
          Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(fse.Obj), new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs);
          builder.Add(cmd);
          // assume $IsGoodHeap($Heap);
          builder.Add(AssumeGoodHeap(tok, etran));
        } else {
          SeqSelectExpr sel = (SeqSelectExpr)lhs;
          assert sel.Seq.Type != null && sel.Seq.Type.IsArrayType;
          bRhs = etran.BoxIfNecessary(tok, bRhs, UserDefinedType.ArrayElementType(sel.Seq.Type));
          if (sel.SelectOne) {
            assert sel.E0 != null;
            Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0));
            // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj,index];
            builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName), "assignment may update an array not in the enclosing method's modifies clause"));
            
            Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr;  // TODO: is this cast always justified?
            Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(sel.Seq), fieldName, bRhs);
            builder.Add(cmd);
            // assume $IsGoodHeap($Heap);
            builder.Add(AssumeGoodHeap(tok, etran));
          } else {
            Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);
            Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq)) : etran.TrExpr(sel.E1);
            // check frame:
            // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);
            Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
            Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(tok, iVar);
            Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));
            Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, ie);
            Bpl.Expr cons = Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName);
            Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
            builder.Add(Assert(tok, q, "assignment may update an array not in the enclosing method's modifies clause"));
            // do the update:  call UpdateArrayRange(arr, low, high, rhs);
            builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
              new Bpl.ExprSeq(etran.TrExpr(sel.Seq), low, high, bRhs),
              new Bpl.IdentifierExprSeq()));
          }
        }
        
      } else if (rhs is HavocRhs) {
        assert lhs is IdentifierExpr;  // for this kind of RHS, the LHS is restricted to be a simple variable
        Bpl.IdentifierExpr x = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?
        builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(x)));

      } else {
        assert rhs is TypeRhs;  // otherwise, an unexpected AssignmentRhs
        TypeRhs tRhs = (TypeRhs)rhs;
        assert lhs is IdentifierExpr;  // for this kind of RHS, the LHS is restricted to be a simple variable
        
        if (tRhs.ArraySize != null) {
          CheckWellformed(tRhs.ArraySize, null, Position.Positive, locals, builder, etran);
          builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(tRhs.ArraySize)), "array size might be negative"));
        }
        
        Bpl.IdentifierExpr nw = GetNewVar_IdExpr(tok, locals);
        builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(nw)));
        // assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
        Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);
        Bpl.Expr rightType;
        if (tRhs.ArraySize != null) {
          // array allocation
          List<Type!> typeArgs = new List<Type!>();
          typeArgs.Add(tRhs.EType);
          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array", predef.ClassNameType), typeArgs, true);
        } else if (tRhs.EType is ObjectType) {
          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type!>(), true);
        } else {
          rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
        }
        builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));
        if (tRhs.ArraySize != null) {
          // assume Array#Length($nw) == arraySize;
          Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw);
          builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(tRhs.ArraySize))));
        }
        // $Heap[$nw, alloc] := true;
        Bpl.Expr alloc = predef.Alloc(tok);
        Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr, nw, alloc, Bpl.Expr.True);
        builder.Add(cmd);
        // x := $nw;
        Bpl.IdentifierExpr x = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?
        builder.Add(Bpl.Cmd.SimpleAssign(tok, x, nw));
        // assume $IsGoodHeap($Heap);
        builder.Add(AssumeGoodHeap(tok, etran));
      }
    }
    
    Bpl.AssumeCmd! AssumeGoodHeap(IToken! tok, ExpressionTranslator! etran) {
      return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr));
    }
    
    // ----- Expression ---------------------------------------------------------------------------
    
    internal class ExpressionTranslator {
      public readonly Bpl.Expr! HeapExpr;
      public readonly PredefinedDecls! predef;
      public readonly Translator! translator;
      readonly Function applyLimited_CurrentFunction;
      
      public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, IToken! heapToken) {
        this.translator = translator;
        this.predef = predef;
        HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
      }
      
      public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap) {
        this.translator = translator;
        this.predef = predef;
        this.HeapExpr = heap;
      }
      
      ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, Function applyLimited_CurrentFunction) {
        this.translator = translator;
        this.predef = predef;
        this.HeapExpr = heap;
        this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
      }

      ExpressionTranslator oldEtran;
      public ExpressionTranslator! Old {
        get {
          if (oldEtran == null) {
            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction);
          }
          return oldEtran;
        }
      }
      
      public ExpressionTranslator! LimitedFunctions(Function! applyLimited_CurrentFunction) {
        return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);
      }
      
      public Bpl.IdentifierExpr! TheFrame(IToken! tok)
        ensures result.Type != null;
      {
        Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta");
        Bpl.Type fieldAlpha = predef.FieldName(tok, alpha);
        Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool);
        return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
      }
      
      public Bpl.IdentifierExpr! ModuleContextHeight()
        ensures result.Type != null;
      {
        return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);
      }

      public Bpl.IdentifierExpr! FunctionContextHeight()
        ensures result.Type != null;
      {
        return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int);
      }

      public Bpl.IdentifierExpr! InMethodContext()
        ensures result.Type != null;
      {
        return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool);
      }

      public Bpl.Expr! TrExpr(Expression! expr)
        requires predef != null;
      {
        if (expr is LiteralExpr) {
          LiteralExpr e = (LiteralExpr)expr;
          if (e.Value == null) {
            return predef.Null;
          } else if (e.Value is bool) {
            return Bpl.Expr.Literal((bool)e.Value);
          } else if (e.Value is BigInteger) {
            return Bpl.Expr.Literal(Microsoft.Basetypes.BigNum.FromBigInt((BigInteger)e.Value));
          } else {
            assert false;  // unexpected literal
          }
          
        } else if (expr is ThisExpr) {
          return new Bpl.IdentifierExpr(expr.tok, "this", predef.RefType);
          
        } else if (expr is IdentifierExpr) {
          IdentifierExpr e = (IdentifierExpr)expr;
          return TrVar(expr.tok, (!)e.Var);
        
        } else if (expr is SetDisplayExpr) {
          SetDisplayExpr e = (SetDisplayExpr)expr;
          Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
          foreach (Expression ee in e.Elements) {
            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), (!)ee.Type);
            s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);
          }
          return s;
          
        } else if (expr is SeqDisplayExpr) {
          SeqDisplayExpr e = (SeqDisplayExpr)expr;
          Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
          int i = 0;
          foreach (Expression ee in e.Elements) {
            Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), (!)ee.Type);
            s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, Bpl.Expr.Literal(i), ss, Bpl.Expr.Literal(i+1));
            i++;
          }
          return s;
        
        } else if (expr is FieldSelectExpr) {
          FieldSelectExpr e = (FieldSelectExpr)expr;
          Bpl.Expr result = Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Obj), new Bpl.IdentifierExpr(expr.tok, translator.GetField((!)e.Field)));
          return CondApplyUnbox(expr.tok, result, e.Field.Type, (!)expr.Type);
          
        } else if (expr is SeqSelectExpr) {
          SeqSelectExpr e = (SeqSelectExpr)expr;
          Bpl.Expr seq = TrExpr(e.Seq);
          Type elmtType;
          assert e.Seq.Type != null;  // the expression has been successfully resolved
          if (e.Seq.Type.IsArrayType) {
            assert e.SelectOne;  // resolution enforces that a non-unit array selections is allowed only as an assignment LHS
            elmtType = UserDefinedType.ArrayElementType(e.Seq.Type);
          } else {
            elmtType = ((SeqType)e.Seq.Type).Arg;
          }
          Bpl.Type elType = translator.TrType(elmtType);
          Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);
          Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);
          if (e.SelectOne) {
            assert e1 == null;
            Bpl.Expr x;
            if (e.Seq.Type.IsArrayType) {
              Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);
              x = Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);
            } else {
              x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
            }
            if (!ModeledAsBoxType(elmtType)) {
              x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
            }
            return x;
          } else {
            if (e1 != null) {
              seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqTake, elType, seq, e1);
            }
            if (e0 != null) {
              seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0);
            }
            return seq;
          }
        
        } else if (expr is SeqUpdateExpr) {
          SeqUpdateExpr e = (SeqUpdateExpr)expr;
          Bpl.Expr seq = TrExpr(e.Seq);
          Type elmtType = ((SeqType!)e.Seq.Type).Arg;
          Bpl.Expr index = TrExpr(e.Index);
          Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
          return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
        
        } else if (expr is FunctionCallExpr) {
          FunctionCallExpr e = (FunctionCallExpr)expr;
          string nm = ((!)e.Function).FullName;
          if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive && !e.Function.IsUnlimited) {
            ModuleDecl module = ((!)e.Function.EnclosingClass).Module;
            if (module == ((!)applyLimited_CurrentFunction.EnclosingClass).Module) {
              if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
                nm += "#limited";
              }
            }
          }
          Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type));
          Bpl.ExprSeq args = new Bpl.ExprSeq();
          args.Add(HeapExpr);
          if (!e.Function.IsStatic) {
            args.Add(TrExpr(e.Receiver));
          }
          for (int i = 0; i < e.Args.Count; i++) {
            Expression ee = e.Args[i];
            Type t = e.Function.Formals[i].Type;
            args.Add(CondApplyBox(expr.tok, TrExpr(ee), (!)ee.Type, t));
          }
          Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);
          return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);
        
        } else if (expr is DatatypeValue) {
          DatatypeValue dtv = (DatatypeValue)expr;
          assert dtv.Ctor != null;  // since dtv has been successfully resolved
          Bpl.ExprSeq args = new Bpl.ExprSeq();
          for (int i = 0; i < dtv.Arguments.Count; i++) {
            Expression arg = dtv.Arguments[i];
            Type t = dtv.Ctor.Formals[i].Type;
            args.Add(CondApplyBox(expr.tok, TrExpr(arg), (!)arg.Type, t));
          }
          Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
          return new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
            
        } else if (expr is OldExpr) {
          OldExpr e = (OldExpr)expr;
          return new Bpl.OldExpr(expr.tok, TrExpr(e.E));
        
        } else if (expr is FreshExpr) {
          FreshExpr e = (FreshExpr)expr;
          Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);
          if (e.E.Type is SetType) {
            // generate:  (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
            // TODO: trigger?
            Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
            Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
            Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
            Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap));
            Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
            return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);
          } else if (e.E.Type is SeqType) {
            // generate:  (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Seq#Index(X,$i),alloc])
            // TODO: trigger?
            Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
            Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
            Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
            Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));
            Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);
            Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
            return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);
          } else {
            // generate:  x == null || !old($Heap)[x]
            Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null);
            Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));
            return Bpl.Expr.Or(oNull, oIsFresh);
          }
        
        } else if (expr is UnaryExpr) {
          UnaryExpr e = (UnaryExpr)expr;
          Bpl.Expr arg = TrExpr(e.E);
          switch (e.Op) {
            case UnaryExpr.Opcode.Not:
              return Bpl.Expr.Not(arg);
            case UnaryExpr.Opcode.SeqLength:
              if (e.E.Type is SeqType) {
                return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
              } else {
                return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg);
              }
            default:
              assert false;  // unexpected unary expression
          }
        
        } else if (expr is BinaryExpr) {
          BinaryExpr e = (BinaryExpr)expr;
          Bpl.Expr e0 = TrExpr(e.E0);
          if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
            return TrInSet(expr.tok, e0, e.E1, (!)e.E0.Type);  // let TrInSet translate e.E1
          } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
            Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, (!)e.E0.Type);  // let TrInSet translate e.E1
            return Bpl.Expr.Not(arg);
          }
          Bpl.Expr e1 = TrExpr(e.E1);
          switch (e.ResolvedOp) {
            case BinaryExpr.ResolvedOpcode.Iff:
              return Bpl.Expr.Iff(e0, e1);
            case BinaryExpr.ResolvedOpcode.Imp:
              return Bpl.Expr.Imp(e0, e1);
            case BinaryExpr.ResolvedOpcode.And:
              return Bpl.Expr.And(e0, e1);
            case BinaryExpr.ResolvedOpcode.Or:
              return Bpl.Expr.Or(e0, e1);
              
            case BinaryExpr.ResolvedOpcode.EqCommon:
              return Bpl.Expr.Eq(e0, e1);
            case BinaryExpr.ResolvedOpcode.NeqCommon:
              return Bpl.Expr.Neq(e0, e1);
              
            case BinaryExpr.ResolvedOpcode.Lt:
              return Bpl.Expr.Lt(e0, e1);
            case BinaryExpr.ResolvedOpcode.Le:
              return Bpl.Expr.Le(e0, e1);
            case BinaryExpr.ResolvedOpcode.Ge:
              return Bpl.Expr.Ge(e0, e1);
            case BinaryExpr.ResolvedOpcode.Gt:
              return Bpl.Expr.Gt(e0, e1);
            case BinaryExpr.ResolvedOpcode.Add:
              return Bpl.Expr.Add(e0, e1);
            case BinaryExpr.ResolvedOpcode.Sub:
              return Bpl.Expr.Sub(e0, e1);
            case BinaryExpr.ResolvedOpcode.Mul:
              return Bpl.Expr.Mul(e0, e1);
            case BinaryExpr.ResolvedOpcode.Div:
              return Bpl.Expr.Div(e0, e1);
            case BinaryExpr.ResolvedOpcode.Mod:
              return Bpl.Expr.Mod(e0, e1);

            case BinaryExpr.ResolvedOpcode.SetEq:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1);
            case BinaryExpr.ResolvedOpcode.SetNeq:
              return Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1));
            case BinaryExpr.ResolvedOpcode.ProperSubset:
              return ProperSubset(expr.tok, e0, e1);
            case BinaryExpr.ResolvedOpcode.Subset:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1);
            case BinaryExpr.ResolvedOpcode.Superset:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e1, e0);
            case BinaryExpr.ResolvedOpcode.ProperSuperset:
              return Bpl.Expr.And(
                translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e1, e0),
                Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1)));
            case BinaryExpr.ResolvedOpcode.Disjoint:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetDisjoint, null, e0, e1);
            case BinaryExpr.ResolvedOpcode.InSet:
              assert false;  // this case handled above
            case BinaryExpr.ResolvedOpcode.Union:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(((SetType!)expr.Type).Arg), e0, e1);
            case BinaryExpr.ResolvedOpcode.Intersection:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(((SetType!)expr.Type).Arg), e0, e1);
            case BinaryExpr.ResolvedOpcode.SetDifference:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(((SetType!)expr.Type).Arg), e0, e1);

            case BinaryExpr.ResolvedOpcode.SeqEq:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1);
            case BinaryExpr.ResolvedOpcode.SeqNeq:
              return Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1));
            case BinaryExpr.ResolvedOpcode.ProperPrefix:
              return ProperPrefix(expr.tok, e0, e1);
            case BinaryExpr.ResolvedOpcode.Prefix:
              {
                Bpl.Expr len0 = translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, e0);
                Bpl.Expr len1 = translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, e1);
                return Bpl.Expr.And(
                  Bpl.Expr.Le(len0, len1),
                  translator.FunctionCall(expr.tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
              }
            case BinaryExpr.ResolvedOpcode.Concat:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(((SeqType!)expr.Type).Arg), e0, e1);
            case BinaryExpr.ResolvedOpcode.InSeq:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1,
                       BoxIfNecessary(expr.tok, e0, (!)e.E0.Type));
            case BinaryExpr.ResolvedOpcode.NotInSeq:
              Bpl.Expr arg = translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1,
                       BoxIfNecessary(expr.tok, e0, (!)e.E0.Type));
              return Bpl.Expr.Not(arg);

            case BinaryExpr.ResolvedOpcode.RankLt:
              return Bpl.Expr.Lt(
                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),
                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));
            case BinaryExpr.ResolvedOpcode.RankGt:
              return Bpl.Expr.Gt(
                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),
                translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));
              
            default:
              assert false;  // unexpected binary expression
          }
        
        } else if (expr is QuantifierExpr) {
          QuantifierExpr e = (QuantifierExpr)expr;
          Bpl.VariableSeq bvars = new Bpl.VariableSeq();
          foreach (BoundVar bv in e.BoundVars) {
            bvars.Add(new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type))));
          }
          Bpl.QKeyValue kv = TrAttributes(e.Attributes);
          Bpl.Trigger tr = null;
          for (Triggers trigs = e.Trigs; trigs != null; trigs = trigs.Prev) {
            Bpl.ExprSeq tt = new Bpl.ExprSeq();
            foreach (Expression term in trigs.Terms) {
              tt.Add(TrExpr(term));
            }
            tr = new Bpl.Trigger(expr.tok, true, tt, tr);
          }
          Bpl.Expr body = TrExpr(e.Body);
          
          if (e is ForallExpr) {
            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, body);
          } else {
            assert e is ExistsExpr;
            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, body);
          }
        
        } else if (expr is ITEExpr) {
          ITEExpr e = (ITEExpr)expr;
          Bpl.Expr g = TrExpr(e.Test);
          Bpl.Expr thn = TrExpr(e.Thn);
          Bpl.Expr els = TrExpr(e.Els);
          return translator.FunctionCall(expr.tok, BuiltinFunction.IfThenElse, translator.TrType((!)expr.Type), g, thn, els);
           
        } else if (expr is BoxingCastExpr) {
          BoxingCastExpr e = (BoxingCastExpr)expr;
          return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
          
        } else if (expr is UnboxingCastExpr) {
          UnboxingCastExpr e = (UnboxingCastExpr)expr;
          return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);
          
        } else {
          assert false;  // unexpected expression
        }
      }
      
      public Bpl.Expr! ProperSubset(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
        return Bpl.Expr.And(
          translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1),
          Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e1, e0)));
      }
      public Bpl.Expr! ProperPrefix(IToken! tok, Bpl.Expr! e0, Bpl.Expr! e1) {
        Bpl.Expr len0 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
        Bpl.Expr len1 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
        return Bpl.Expr.And(
          Bpl.Expr.Lt(len0, len1),
          translator.FunctionCall(tok, BuiltinFunction.SeqSameUntil, null, e0, e1, len0));
      }

      public Bpl.Expr! TrUseExpr(FunctionCallExpr! e)
        requires e.Function != null && e.Type != null;
      {
        Function fn = e.Function;
        Bpl.ExprSeq args = new Bpl.ExprSeq();
        args.Add(HeapExpr);
        if (!fn.IsStatic) {
          args.Add(TrExpr(e.Receiver));
        }
        foreach (Expression ee in e.Args) {
          args.Add(TrExpr(ee));
        }
        Bpl.Expr f0 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName, translator.TrType(e.Type))), args);
        Bpl.Expr f1;
        if (fn.IsRecursive && !fn.IsUnlimited) {
          f1 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName + "#limited", translator.TrType(e.Type))), args);
        } else {
          f1 = f0;
        }
        return Bpl.Expr.Eq(f0, f1);
      }

      public Bpl.Expr! CondApplyBox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
        if (!ModeledAsBoxType(fromType) && ModeledAsBoxType(toType)) {
          return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
        } else {
          return e;
        }
      }
      
      public Bpl.Expr! BoxIfNecessary(IToken! tok, Bpl.Expr! e, Type! fromType) {
        if (!ModeledAsBoxType(fromType)) {
          return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
        } else {
          return e;
        }
      }
      
      public Bpl.Expr! CondApplyUnbox(IToken! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
        if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) {
          return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);
        } else {
          return e;
        }
      }
      
      public static bool ModeledAsBoxType(Type! t) {
        while (true) {
          TypeProxy tp = t as TypeProxy;
          if (tp == null) {
            break;
          } else if (tp.T == null) {
            // unresolved proxy
            return false;
          } else {
            t = tp.T;
          }
        }
        return t.IsTypeParameter;
      }

      public Bpl.IdentifierExpr! TrVar(IToken! tok, IVariable! var) {
        return new Bpl.IdentifierExpr(tok, var.UniqueName, translator.TrType(var.Type));
      }
      
      /// <summary>
      /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the
      /// translation, because such functions can mess up triggering.
      /// </summary>
      public Bpl.Expr! TrInSet(IToken! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {
        if (s is BinaryExpr) {
          BinaryExpr bin = (BinaryExpr)s;
          switch (bin.ResolvedOp) {
            case BinaryExpr.ResolvedOpcode.Union:
              return Bpl.Expr.Or(TrInSet(tok, elmt, bin.E0, elmtType), TrInSet(tok, elmt, bin.E1, elmtType));
            case BinaryExpr.ResolvedOpcode.Intersection:
              return Bpl.Expr.And(TrInSet(tok, elmt, bin.E0, elmtType), TrInSet(tok, elmt, bin.E1, elmtType));
            case BinaryExpr.ResolvedOpcode.SetDifference:
              return Bpl.Expr.And(TrInSet(tok, elmt, bin.E0, elmtType), Bpl.Expr.Not(TrInSet(tok, elmt, bin.E1, elmtType)));
            default:
              break;
          }
        } else if (s is SetDisplayExpr) {
          SetDisplayExpr disp = (SetDisplayExpr)s;
          Bpl.Expr disjunction = null;
          foreach (Expression a in disp.Elements) {
            Bpl.Expr disjunct = Bpl.Expr.Eq(elmt, TrExpr(a));
            if (disjunction == null) {
              disjunction = disjunct;
            } else {
              disjunction = Bpl.Expr.Or(disjunction, disjunct);
            }
          }
          if (disjunction == null) {
            return Bpl.Expr.False;
          } else {
            return disjunction;
          }
        }
        return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));
      }
      
      Bpl.QKeyValue TrAttributes(Attributes attrs) {
        Bpl.QKeyValue kv = null;
        while (attrs != null) {
          List<object!> parms = new List<object!>();
          foreach (Attributes.Argument arg in attrs.Args) {
            if (arg.E != null) {
              parms.Add(TrExpr(arg.E));
            } else {
              parms.Add((!)arg.S);
            }
          }
          kv = new Bpl.QKeyValue(Token.NoToken, attrs.Name, parms, kv);
          attrs = attrs.Prev;
        }
        return kv;
      }
      
      // --------------- help routines ---------------

      public Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e) {
        return IsAlloced(tok, e, HeapExpr);
      }
          
      Bpl.Expr! IsAlloced(IToken! tok, Bpl.Expr! e, Bpl.Expr! heap) {
        return Bpl.Expr.SelectTok(tok, heap, e, predef.Alloc(tok));
      }
      
      public Bpl.Expr! GoodRef(IToken! tok, Bpl.Expr! e, Type! type) {
        Bpl.Expr goodRef;
        if (type is UserDefinedType && ((UserDefinedType)type).ResolvedClass != null) {
          // Heap[e, alloc] && dtype(e) == T
          return GoodRef_Class(tok, e, (UserDefinedType)type, false);
        } else {
          // Heap[e, alloc]
          return IsAlloced(tok, e);
        }
      }
      
      public Bpl.Expr! GoodRef_Class(IToken! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
        requires type.ResolvedClass is ClassDecl;
      {
        return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);
      }
      
      public Bpl.Expr! GoodRef_Ref(IToken! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {
        // Heap[e, alloc]
        Bpl.Expr r = IsAlloced(tok, e);
        if (isNew) {
          r = Bpl.Expr.Not(r);  // use the conjunct:  !Heap[e, alloc]
        }
        
        // dtype(e) == C
        Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);
        Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);
        r = Bpl.Expr.And(r, dtype);
        
        // dtypeParams(e, #) == T
        int n = 0;
        foreach (Type arg in typeArgs) {
          Bpl.Expr tpFunc = translator.FunctionCall(tok, BuiltinFunction.TypeParams, null, e, Bpl.Expr.Literal(n));
          Bpl.Expr ta = translator.GetTypeExpr(tok, arg);
          if (ta != null) {
            r = Bpl.Expr.And(r, Bpl.Expr.Eq(tpFunc, ta));
          }
          n++;
        }
        
        return r;
      }
      
      public Bpl.Expr TypeAlloced(IToken! tok, Bpl.Expr! e, Type! type) {
        while (true) {
          TypeProxy proxy = type as TypeProxy;
          if (proxy == null) {
            break;
          } else if (proxy.T == null) {
            return null;
          } else {
            type = proxy.T;
          }
        }
        
        Bpl.BoundVariable bv = null;
        Bpl.Expr ante = null;
        if (type.IsRefType) {  // object or class type
          // e == null || $Heap[e, alloc]
          // This is done below
          
        } else if (type is SetType) {
          // (forall tp: BoxType :: e[tp] ==> Unbox(tp) == null || $Heap[Unbox(tp), alloc])
          bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$tp", predef.BoxType));
          Bpl.Expr tp = new Bpl.IdentifierExpr(tok, bv);
          ante = Bpl.Expr.SelectTok(tok, e, tp);  // note, this means the set-inclusion does not undergo the set-inclusion expansion optimization done by TrInSet
          e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, tp);
          
        } else if (type is SeqType) {
          // (forall i: int :: Unbox(Seq#Index(e,i)) == null || $Heap[Unbox(Seq#Index(e,i)), alloc])
          bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
          e = translator.FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, e, new Bpl.IdentifierExpr(tok, bv));
          e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, e);
          
        } else {
          return null;
        }
        
        Bpl.Expr r = Bpl.Expr.Or(Bpl.Expr.Eq(e, predef.Null), GoodRef(tok, e, type));
        if (ante != null) {
          r = Bpl.Expr.Imp(ante, r);
        }
        if (bv != null) {
          r = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(bv), r);
        }
        return r;
      }
    }
    
    enum BuiltinFunction {
      SetEmpty,
      SetUnionOne,
      SetUnion,
      SetIntersection,
      SetDifference,
      SetEqual,
      SetSubset,
      SetDisjoint,
      
      SeqLength,
      SeqEmpty,
      SeqBuild,
      SeqAppend,
      SeqIndex,
      SeqUpdate,
      SeqContains,
      SeqDrop,
      SeqTake,
      SeqEqual,
      SeqSameUntil,
      
      ArrayLength,
      IndexField,
      
      IfThenElse,
      
      Box,
      Unbox,
      
      IsGoodHeap,
      HeapSucc,
      
      DynamicType,  // allocated type
      TypeParams,   // type parameters to allocated type
      TypeTuple,
      DeclType,
      FCat,  // field category (indexed or named)
      
      DatatypeCtorId,
      DtRank,
      
      // CEV
      CevInit,
      CevVarIntro,
      CevVarUpdate,
      CevControlFlowEvent,
      CevProgramLocation,
    }
    
    // The "typeInstantiation" argument is passed in to help construct the result type of the function.
    Bpl.NAryExpr! FunctionCall(IToken! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)
      requires predef != null;
    {
      switch (f) {
        case BuiltinFunction.SetEmpty: {
          assert args.Length == 0;
          assert typeInstantiation != null;
          Bpl.Type resultType = predef.SetType(tok, typeInstantiation);
          return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Set#Empty", resultType, args), resultType);
        }
        case BuiltinFunction.SetUnionOne:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Set#UnionOne", predef.SetType(tok, typeInstantiation), args);
        case BuiltinFunction.SetUnion:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Set#Union", predef.SetType(tok, typeInstantiation), args);
        case BuiltinFunction.SetIntersection:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Set#Intersection", predef.SetType(tok, typeInstantiation), args);
        case BuiltinFunction.SetDifference:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Set#Difference", predef.SetType(tok, typeInstantiation), args);
        case BuiltinFunction.SetEqual:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Set#Equal", Bpl.Type.Bool, args);
        case BuiltinFunction.SetSubset:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Set#Subset", Bpl.Type.Bool, args);
        case BuiltinFunction.SetDisjoint:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);

        case BuiltinFunction.SeqLength:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Seq#Length", Bpl.Type.Int, args);
        case BuiltinFunction.SeqEmpty: {
          assert args.Length == 0;
          assert typeInstantiation != null;
          Bpl.Type resultType = predef.SeqType(tok, typeInstantiation);
          return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType);
        }
        case BuiltinFunction.SeqBuild:
          assert args.Length == 4;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Build", predef.SeqType(tok, typeInstantiation), args);
        case BuiltinFunction.SeqAppend:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Append", predef.SeqType(tok, typeInstantiation), args);
        case BuiltinFunction.SeqIndex:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Index", typeInstantiation, args);
        case BuiltinFunction.SeqUpdate:
          assert args.Length == 3;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Update", predef.SeqType(tok, typeInstantiation), args);
        case BuiltinFunction.SeqContains:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Seq#Contains", Bpl.Type.Bool, args);
        case BuiltinFunction.SeqDrop:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Drop", predef.SeqType(tok, typeInstantiation), args);
        case BuiltinFunction.SeqTake:
          assert args.Length == 2;
          assert typeInstantiation != null;
          return FunctionCall(tok, "Seq#Take", predef.SeqType(tok, typeInstantiation), args);
        case BuiltinFunction.SeqEqual:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Seq#Equal", Bpl.Type.Bool, args);
        case BuiltinFunction.SeqSameUntil:
          assert args.Length == 3;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
          
        case BuiltinFunction.ArrayLength:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "Array#Length", Bpl.Type.Int, args);
        case BuiltinFunction.IndexField:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "IndexField", predef.FieldName(tok, predef.BoxType), args);

        case BuiltinFunction.IfThenElse:
          assert args.Length == 3;
          assert typeInstantiation != null;
          return FunctionCall(tok, "$ite", typeInstantiation, args);

        case BuiltinFunction.Box:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "$Box", predef.BoxType, args);
        case BuiltinFunction.Unbox:
          assert args.Length == 1;
          assert typeInstantiation != null;
          return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);

        case BuiltinFunction.IsGoodHeap:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "$IsGoodHeap", Bpl.Type.Bool, args);
        case BuiltinFunction.HeapSucc:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "$HeapSucc", Bpl.Type.Bool, args);

        case BuiltinFunction.DynamicType:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "dtype", predef.ClassNameType, args);
        case BuiltinFunction.TypeParams:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "TypeParams", predef.ClassNameType, args);
        case BuiltinFunction.TypeTuple:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args);
        case BuiltinFunction.DeclType:
          assert args.Length == 1;
          assert typeInstantiation != null;
          return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
        case BuiltinFunction.FCat:
          assert args.Length == 1;
          assert typeInstantiation != null;
          return FunctionCall(tok, "FCat", predef.FieldCategoryType, args);
          
        case BuiltinFunction.DatatypeCtorId:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "DatatypeCtorId", predef.DtCtorId, args);
        case BuiltinFunction.DtRank:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "DtRank", Bpl.Type.Int, args);
          
        case BuiltinFunction.CevInit:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "#cev_init", Bpl.Type.Bool, args);
        case BuiltinFunction.CevVarIntro:
          assert args.Length == 5;
          assert typeInstantiation == null;
          return FunctionCall(tok, "#cev_var_intro", Bpl.Type.Bool, args);
        case BuiltinFunction.CevVarUpdate:
          assert args.Length == 4;
          assert typeInstantiation == null;
          return FunctionCall(tok, "#cev_var_update", Bpl.Type.Bool, args);
        case BuiltinFunction.CevControlFlowEvent:
          assert args.Length == 2;
          assert typeInstantiation == null;
          return FunctionCall(tok, "#cev_control_flow_event", Bpl.Type.Bool, args);
        case BuiltinFunction.CevProgramLocation:
          assert args.Length == 1;
          assert typeInstantiation == null;
          return FunctionCall(tok, "#cev_save_position", predef.CevTokenType, args);
           
        default:
          assert false;  // unexpected built-in function
      }
    }
    
    Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)
    {
      return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), new Bpl.ExprSeq(args));
    }

    Bpl.NAryExpr! FunctionCall(IToken! tok, string! function, Bpl.Type! returnType, List<Bpl.Expr!>! args)
    {
      Bpl.ExprSeq aa = new Bpl.ExprSeq();
      foreach (Bpl.Expr arg in args) {
        aa.Add(arg);
      }
      return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), aa);
    }

    public bool SplitExpr(Expression! expr, out List<Expression!>! definitions, out List<Expression!>! pieces) {
      definitions = new List<Expression!>();
      pieces = new List<Expression!>();
      return SplitExpr(expr, true, definitions, pieces);
    }

    ///<summary>
    /// Returns false if no split occurred (in that case, nothing was added to definitions, and (exactly) expr itself was added to pieces.
    ///</summary>
    public bool SplitExpr(Expression! expr, bool expandFunctions, List<Expression!>! definitions, List<Expression!>! pieces)
      requires expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType);
    {
      if (expr is BoxingCastExpr) {
        BoxingCastExpr bce = (BoxingCastExpr)expr;
        List<Expression!> pp = new List<Expression!>();
        if (SplitExpr(bce.E, expandFunctions, definitions, pp)) {
          foreach (Expression e in pp) {
            Expression r = new BoxingCastExpr(e, bce.FromType, bce.ToType);
            r.Type = bce.ToType;  // resolve here
            pieces.Add(r);
          }
          return true;
        }
        
      } else if (expr is BinaryExpr) {
        BinaryExpr bin = (BinaryExpr)expr;
        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
          SplitExpr(bin.E0, expandFunctions, definitions, pieces);
          SplitExpr(bin.E1, expandFunctions, definitions, pieces);
          return true;
        
        } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
          List<Expression!> pp = new List<Expression!>();
          if (SplitExpr(bin.E1, expandFunctions, definitions, pp)) {
            foreach (Expression e in pp) {
              BinaryExpr r = new BinaryExpr(e.tok, bin.Op, bin.E0, e);
              r.ResolvedOp = bin.ResolvedOp;  r.Type = bin.Type;  // resolve on the fly
              pieces.Add(r);
            }
            return true;
          }
        }
      
      } else if (expr is ITEExpr) {
        ITEExpr ite = (ITEExpr)expr;

        List<Expression!> pp = new List<Expression!>();
        SplitExpr(ite.Thn, expandFunctions, definitions, pp);
        foreach (Expression e in pp) {
          BinaryExpr r = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, ite.Test, e);
          r.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  r.Type = ite.Type;  // resolve on the fly
          pieces.Add(r);
        }

        Expression negatedGuard = new UnaryExpr(ite.Test.tok, UnaryExpr.Opcode.Not, ite.Test);
        negatedGuard.Type = ite.Test.Type;  // resolve on the fly
        pp = new List<Expression!>();
        SplitExpr(ite.Els, expandFunctions, definitions, pp);
        foreach (Expression e in pp) {
          BinaryExpr r = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, negatedGuard, e);
          r.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  r.Type = ite.Type;  // resolve on the fly
          pieces.Add(r);
        }
        return true;
      
      } else if (expr is OldExpr) {
        List<Expression!> dd = new List<Expression!>(), pp = new List<Expression!>();
        if (SplitExpr(((OldExpr)expr).E, expandFunctions, dd, pp)) {
          foreach (Expression e in dd) {
            Expression r = new OldExpr(expr.tok, e);
            r.Type = Type.Bool;  // resolve here
            definitions.Add(r);
          }
          foreach (Expression e in pp) {
            Expression r = new OldExpr(expr.tok, e);
            r.Type = e.Type;  // resolve here
            pieces.Add(r);
          }
          return true;
        }
        
      } else if (expandFunctions && expr is FunctionCallExpr) {
        FunctionCallExpr fexp = (FunctionCallExpr)expr;
        assert fexp.Function != null;  // filled in during resolution
        if (fexp.Function.Body != null && !(fexp.Function.Body is MatchExpr)) {
          // inline this body
          Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
          assert fexp.Args.Count == fexp.Function.Formals.Count;
          for (int i = 0; i < fexp.Function.Formals.Count; i++) {
            Formal p = fexp.Function.Formals[i];
            Expression arg = fexp.Args[i];
            arg = new BoxingCastExpr(arg, (!)arg.Type, p.Type);
            arg.Type = p.Type;  // resolve here
            substMap.Add(p, arg);
          }
          Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);

          // add definition:  fn(args) ==> body
          Expression bodyx = new UnboxingCastExpr(body, fexp.Function.ResultType, (!)expr.Type);
          bodyx.Type = expr.Type;  // resolve here
          BinaryExpr def = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, fexp, bodyx);
          def.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  def.Type = Type.Bool;  // resolve on the fly
          definitions.Add(def);

          // recurse on body
          List<Expression!> pp = new List<Expression!>();
          SplitExpr(body, false, definitions, pp);
          foreach (Expression e in pp) {
            Expression r = new UnboxingCastExpr(e, fexp.Function.ResultType, expr.Type);
            r.Type = expr.Type;  // resolve here
            pieces.Add(r);
          }
          return true;
        }
      }

      pieces.Add(expr); 
      return false;
    }
    
    static Expression! Substitute(Expression! expr, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
      Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
      
      if (expr is LiteralExpr || expr is WildcardExpr) {
        // nothing to substitute
      } else if (expr is ThisExpr) {
        return receiverReplacement == null ? expr : receiverReplacement;
      } else if (expr is IdentifierExpr) {
        IdentifierExpr e = (IdentifierExpr)expr;
        Expression substExpr;
        if (substMap.TryGetValue(e.Var, out substExpr)) {
          return (!)substExpr;
        }
      } else if (expr is DisplayExpression) {
        DisplayExpression e = (DisplayExpression)expr;
        List<Expression!> newElements = SubstituteExprList(e.Elements, receiverReplacement, substMap);
        DisplayExpression newDisplayExpr;
        if (newElements != e.Elements) {
          if (expr is SetDisplayExpr) {
            newExpr = new SetDisplayExpr(expr.tok, newElements);
          } else {
            newExpr = new SeqDisplayExpr(expr.tok, newElements);
          }
        }
        
      } else if (expr is FieldSelectExpr) {
        FieldSelectExpr fse = (FieldSelectExpr)expr;
        Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);
        if (substE != fse.Obj) {
          FieldSelectExpr fseNew = new FieldSelectExpr(fse.tok, substE, fse.FieldName);
          fseNew.Field = fse.Field;  // resolve on the fly (and fseExpr.Type is set at end of method)
          newExpr = fseNew;
        }
        
      } else if (expr is SeqSelectExpr) {
        SeqSelectExpr sse = (SeqSelectExpr)expr;
        Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
        Expression e0 = sse.E0 == null ? null : Substitute(sse.E0, receiverReplacement, substMap);
        Expression e1 = sse.E1 == null ? null : Substitute(sse.E1, receiverReplacement, substMap);
        if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {
          newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
        }
        
      } else if (expr is SeqUpdateExpr) {
        SeqUpdateExpr sse = (SeqUpdateExpr)expr;
        Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
        Expression index = Substitute(sse.Index, receiverReplacement, substMap);
        Expression val = Substitute(sse.Value, receiverReplacement, substMap);
        if (seq != sse.Seq || index != sse.Index || val != sse.Value) {
          newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);
        }
        
      } else if (expr is FunctionCallExpr) {
        FunctionCallExpr e = (FunctionCallExpr)expr;
        Expression receiver = Substitute(e.Receiver, receiverReplacement, substMap);
        List<Expression!> newArgs = SubstituteExprList(e.Args, receiverReplacement, substMap);
        if (receiver != e.Receiver || newArgs != e.Args) {
          FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, newArgs);
          newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)
          newExpr = newFce;
        }
      
      } else if (expr is DatatypeValue) {
        DatatypeValue dtv = (DatatypeValue)expr;
        List<Expression!> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);
        if (newArgs != dtv.Arguments) {
          DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);
          newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)
          newExpr = newDtv;
        }

      } else if (expr is OldExpr) {
        OldExpr e = (OldExpr)expr;
        Expression se = Substitute(e.E, receiverReplacement, substMap);
        if (se != e.E) {
          newExpr = new OldExpr(expr.tok, se);
        }
      } else if (expr is FreshExpr) {
        FreshExpr e = (FreshExpr)expr;
        Expression se = Substitute(e.E, receiverReplacement, substMap);
        if (se != e.E) {
          newExpr = new FreshExpr(expr.tok, se);
        }
      } else if (expr is UnaryExpr) {
        UnaryExpr e = (UnaryExpr)expr;
        Expression se = Substitute(e.E, receiverReplacement, substMap);
        if (se != e.E) {
          newExpr = new UnaryExpr(expr.tok, e.Op, se);
        }
      } else if (expr is BinaryExpr) {
        BinaryExpr e = (BinaryExpr)expr;
        Expression e0 = Substitute(e.E0, receiverReplacement, substMap);
        Expression e1 = Substitute(e.E1, receiverReplacement, substMap);
        if (e0 != e.E0 || e1 != e.E1) {
          BinaryExpr newBin = new BinaryExpr(expr.tok, e.Op, e0, e1);
          newBin.ResolvedOp = e.ResolvedOp;  // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)
          newExpr = newBin;
        }
        
      } else if (expr is QuantifierExpr) {
        QuantifierExpr e = (QuantifierExpr)expr;
        Expression newBody = Substitute(e.Body, receiverReplacement, substMap);
        Triggers newTrigs = SubstTriggers(e.Trigs, receiverReplacement, substMap);
        Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);
        if (newBody != e.Body || newTrigs != e.Trigs || newAttrs != e.Attributes) {
          if (expr is ForallExpr) {
            newExpr = new ForallExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);
          } else {
            newExpr = new ExistsExpr(expr.tok, e.BoundVars, newBody, newTrigs, newAttrs);
          }
        }
        
      } else if (expr is ITEExpr) {
        ITEExpr e = (ITEExpr)expr;
        Expression test = Substitute(e.Test, receiverReplacement, substMap);
        Expression thn = Substitute(e.Thn, receiverReplacement, substMap);
        Expression els = Substitute(e.Els, receiverReplacement, substMap);
        if (test != e.Test || thn != e.Thn || els != e.Els) {
          newExpr = new ITEExpr(expr.tok, test, thn, els);
        }
      }
      
      if (newExpr == null) {
        return expr;
      } else {
        newExpr.Type = expr.Type;  // resolve on the fly (any additional resolution must be done above)
        return newExpr;
      }
    }
    
    static List<Expression!>! SubstituteExprList(List<Expression!>! elist,
                                                 Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
      List<Expression!> newElist = null;  // initialized lazily
      for (int i = 0; i < elist.Count; i++)
        invariant newElist == null || newElist.Count == i;
      {
        Expression substE = Substitute(elist[i], receiverReplacement, substMap);
        if (substE != elist[i] && newElist == null) {
          newElist = new List<Expression!>();
          for (int j = 0; j < i; j++) {
            newElist.Add(elist[j]);
          }
        }
        if (newElist != null) {
          newElist.Add(substE);
        }
      }
      if (newElist == null) {
        return elist;
      } else {
        return newElist;
      }
    }
    
    static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
      if (trigs != null) {
        List<Expression!> terms = SubstituteExprList(trigs.Terms, receiverReplacement, substMap);
        Triggers prev = SubstTriggers(trigs.Prev, receiverReplacement, substMap);
        if (terms != trigs.Terms || prev != trigs.Prev) {
          return new Triggers(terms, prev);
        }
      }
      return trigs;
    }
        
    static Attributes SubstAttributes(Attributes attrs, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
      if (attrs != null) {
        List<Attributes.Argument!> newArgs = new List<Attributes.Argument!>();  // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
        bool anyArgSubst = false;
        foreach (Attributes.Argument arg in attrs.Args) {
          Attributes.Argument newArg = arg;
          if (arg.E != null) {
            Expression newE = Substitute(arg.E, receiverReplacement, substMap);
            if (newE != arg.E) {
              newArg = new Attributes.Argument(newE);
              anyArgSubst = true;
            }
          }
          newArgs.Add(newArg);
        }
        if (!anyArgSubst) {
          newArgs = attrs.Args;
        }
        
        Attributes prev = SubstAttributes(attrs.Prev, receiverReplacement, substMap);
        if (newArgs != attrs.Args || prev != attrs.Prev) {
          return new Attributes(attrs.Name, newArgs, prev);
        }
      }
      return attrs;
    }
        
  }
}