//-----------------------------------------------------------------------------
//
// 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;

// TODO:  totality checks for statements
// TODO:  totality checks for pre/post conditions

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!>();
    readonly Dictionary<Function!,Bpl.Function!>! functions = new Dictionary<Function!,Bpl.Function!>();
    readonly Dictionary<Method!,Bpl.Procedure!>! methods = new Dictionary<Method!,Bpl.Procedure!>();

    // Machinery for providing information to the Counterexample Visualizer
    readonly Dictionary<string!,int>! cevFilenames = new Dictionary<string!,int>();
    readonly Dictionary<Token!,Bpl.Constant!>! cevLocations = new Dictionary<Token!,Bpl.Constant!>();
    readonly Dictionary<string!,Bpl.Constant!>! cevVariables = new Dictionary<string!,Bpl.Constant!>();
    Bpl.Expr! CevLocation(Token! 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(Token! tok, Bpl.Type! ty) {
        return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
      }
      private readonly Bpl.TypeCtorDecl! seqTypeCtor;
      public Bpl.Type! SeqType(Token! tok, Bpl.Type! ty) {
        return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
      }
      readonly Bpl.TypeCtorDecl! fieldName;
      public Bpl.Type! FieldName(Token! 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! DatatypeType;
      public readonly Bpl.Type! DtCtorId;
      public readonly Bpl.Expr! Null;
      private readonly Bpl.Constant! allocField;
      public Bpl.IdentifierExpr! Alloc(Token! 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! 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.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 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 == "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 (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, 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");
      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 (TopLevelDecl d in program.Classes) {
        if (d is DatatypeDecl) {
          AddDatatype((DatatypeDecl)d);
        } else {
          AddClassMembers((ClassDecl)d);
        }
      }
      foreach (TopLevelDecl d in program.Classes) {
        if (d is ClassDecl) {
          ClassDecl c = (ClassDecl)d;
          foreach (MemberDecl member in c.Members) {
            if (member is Method) {
              Method m = (Method)member;
              if (m.Body != null) {
                AddMethodImpl(m);
              }
            } else if (member is Function) {
              Function f = (Function)member;
              AddFrameAxiom(f);
              AddWellformednessCheck(f);
            }
          }
        } else {
          assert d is DatatypeDecl;
        }
      }
      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) {
            // axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));
            CreateBoundVariables(ctor.Formals, out bvs, out args);
            lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, 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));
          }
          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 (MatchCase 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.IsUse) {
              AddUseAxioms(f);
            }
          }
          
        } else if (member is Method) {
          Method m = (Method)member;
          Bpl.Procedure proc = GetMethod(m);
          sink.TopLevelDeclarations.Add(proc);
          
        } 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;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
      
      // axiom (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 #alt form of all "use" functions.
      //
      // 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.
      //
      // TODO: Add a CanAssumeFunctionDefs antecedent to this axiom (see Dafny lecture notes from Marktoberdorf 2008).
      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.IsClass) {
        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));
        }
      }
      
      Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
      if (!f.IsClass) {
        assert bvThisIdExpr != null;  // set to non-null value above when !f.IsClass
        ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante);
      }
      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.AltFunctions.TrExpr(body))));
      return new Bpl.Axiom(f.tok, ax);
    }
    
    void AddUseAxioms(Function! f)
      requires f.IsUse;
      requires sink != null && predef != null;
    {
      // axiom (forall formals :: { f(args) } f(args) == f#alt(args))
      // axiom (forall formals :: { f#use(args) } f#use(args) ==> f(args) == f#alt(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.IsClass) {
        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 altFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#alt", TrType(f.ResultType)));
      Bpl.Expr altFuncAppl = new Bpl.NAryExpr(f.tok, altFuncID, args);
      Bpl.FunctionCall useFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", Bpl.Type.Bool));
      Bpl.Expr useFuncAppl = new Bpl.NAryExpr(f.tok, useFuncID, 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, altFuncAppl));
      sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
      
      tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useFuncAppl));
      ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(useFuncAppl, Bpl.Expr.Eq(origFuncAppl, altFuncAppl)));
      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, 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(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, Bpl.Expr lowerBound, bool includeUpperBound) {
      if (lowerBound == null) {
        lowerBound = Bpl.Expr.Literal(0);
      }
      Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
      Bpl.Expr upper;
      if (includeUpperBound) {
        upper = Bpl.Expr.Le(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
      } else {
        upper = Bpl.Expr.Lt(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
      }
      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(Token! 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(Token! 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)
      requires sink != null && predef != null && m.Body != null;
      requires currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null;
      ensures currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null;
    {
      Bpl.Procedure proc = GetMethod(m);
      currentMethod = m;

      Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
      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 proc.InParams) {
        assert p != null;
        builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
          new Bpl.ExprSeq(
            CevLocation((Dafny.Token)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 proc.OutParams) {
        assert p != null;
        builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
          new Bpl.ExprSeq(
            CevLocation((Dafny.Token)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()));
      }

      Bpl.StmtList stmts = TrStmt2StmtList(builder, m.Body, localVariables, new ExpressionTranslator(this, predef, m.tok));
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
      Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
        typeParams,
        Bpl.Formal.StripWhereClauses(proc.InParams),
        Bpl.Formal.StripWhereClauses(proc.OutParams),
        localVariables, stmts);
      sink.TopLevelDeclarations.Add(impl);
      
      currentMethod = null;
      loopHeapVarCount = 0;
      otherTmpVarCount = 0;
      _phvie = null;
      _nwie = null;
    }
    
    /// <summary>
    /// Generates:
    ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::
    ///        { F(h0,formals), F(h1,formals) }
    ///        heaps are well-formed and formals are allocated
    ///        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])
    ///        AND
    ///        (forall(alpha) o: ref, f: Field alpha ::
    ///            o != null AND h1[o,alloc] AND h0[o,alloc] AND
    ///            o in reads clause of formals in h1
    ///            IMPLIES h0[o,f] == h1[o,f])
    ///        IMPLIES
    ///        F(h0,formals) == F(h1,formals)
    ///      );
    /// Note, the second h?[o,alloc] in the antecedent of each inner forall above is sound
    /// because user expressions are not allowed to quantify over all allocated objects, and
    /// in particular, they have no way to depend on the .alloc field of an object.
    ///
    /// If the function is a "use" function, then "F "in the last line is replaced by "F#alt".
    /// </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, etran0.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 r0 = InRWClause(f.tok, o, f.Reads, etran0, null, null);
      Bpl.Expr r1 = InRWClause(f.tok, o, f.Reads, etran1, 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));
      Bpl.Expr q1 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
        Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r1), 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.IsClass) {
        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); }
      }
      
      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.IsUse ? f.FullName + "#alt" : f.FullName, TrType(f.ResultType)));
      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(F0, F1));
      
      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
        Bpl.Expr.Imp(wellFormed,
        Bpl.Expr.Imp(Bpl.Expr.And(q0, q1), eq)));
      sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));
    }
    
    Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! 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 (Expression rwComponent in rw) {
        Expression e = rwComponent;
        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), 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.Imp(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 (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;
    {
      ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
      // parameters of the procedure
      Bpl.VariableSeq inParams = new Bpl.VariableSeq();
      if (!f.IsClass) {
        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.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
        new Bpl.RequiresSeq(), new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
      sink.TopLevelDeclarations.Add(proc);

      Bpl.VariableSeq locals = new Bpl.VariableSeq();
      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
      // 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 the syntax is
      // 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) {
        CheckWellformed(p, f, Position.Positive, locals, builder, etran);
      }
      // check well-formedness of the body
      if (f.Body != null) {
        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;
        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, 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, 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, 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.IsClass && !(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;
        return IsTotal(e.E, etran);
      } 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(Token! 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) {
        // 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, InRWClause(expr.tok, etran.TrExpr(e.Obj), func.Reads, etran, null, null), "insufficient reads clause to read field"));
        }
      } else if (expr is SeqSelectExpr) {
        SeqSelectExpr e = (SeqSelectExpr)expr;
        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, 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, e0, true), "end-of-range beyond length of sequence"));
        }
      } 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, 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.IsClass && !(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, 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?
          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(e.Args[i]));
          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
          // emit: assert (forall o: ref :: o != null && o in callee.reads ==> o in caller.reads);
          Bpl.BoundVariable 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 oInCallee = InRWClause(expr.tok, o, e.Function.Reads, etran, e.Receiver, substMap);
          Bpl.Expr oInCaller = InRWClause(expr.tok, o, func.Reads, etran, null, null);
          Bpl.Expr q = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInCallee), oInCaller));
          builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));
  
          // finally, check that the decreases measure goes down
          Bpl.Expr decrExpr;
          int N = min{e.Function.Decreases.Count, func.Decreases.Count};
          if (N != 0) {
            // both functions have explicit decreases clauses, so use them
            List<Type!> types = new List<Type!>();
            List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();
            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(e.Function.Decreases[i], e.Receiver, substMap);
              Expression e1 = func.Decreases[i];
              if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {
                break;
              }
              types.Add(e0.Type);
              calleeTotal.Add(IsTotal(e0, etran));
              callee.Add(etran.TrExpr(e0));
              caller.Add(etran.TrExpr(e1));
            }
            decrExpr = DecreasesCheck(expr.tok, types, calleeTotal, callee, caller, builder, etran, "");
          } else {
            // todo:  include totality checks for callee in this branch!
            List<Expression!> d0 = null, d1 = null;
            if (e.Function.Decreases.Count == 0) {
              d0 = e.Function.Reads;  // use its reads clause instead
            } else if (e.Function.Decreases[0].Type is SetType) {
              d0 = new List<Expression!>(1);
              d0.Add(e.Function.Decreases[0]);  // use the first component of the declared decreases clause
            } else {
              d0 = null;  // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause
            }
            if (func.Decreases.Count == 0) {
              d1 = func.Reads;  // use its reads clause instead
            } else if (func.Decreases[0].Type is SetType) {
              d1 = new List<Expression!>(1);
              d1.Add(func.Decreases[0]);  // use the first component of the declared decreases clause
            } else {
              d1 = null;  // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause
            }
            if (d0 == null || d1 == null) {
              decrExpr = Bpl.Expr.False;
            } else {
              oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$d", predef.RefType));
              o = new Bpl.IdentifierExpr(expr.tok, oVar);
              Bpl.Expr r0 = InRWClause(expr.tok, o, d0, etran, e.Receiver, substMap);
              Bpl.Expr r1 = InRWClause(expr.tok, o, d1, etran, null, null);
              Bpl.Expr qSubset = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(r0, r1));
              Bpl.Expr qProper = new Bpl.ExistsExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.And(Bpl.Expr.Not(r0), r1));
              decrExpr = Bpl.Expr.And(qSubset, qProper);
            }
          }
          builder.Add(Assert(expr.tok, decrExpr, "failure to decrease termination measure"));
        }
      } 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 || expr is FreshExpr) {
        assert false;  // unexpected expression in function body
      } 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);
      } 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, 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 (MatchCase 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
      }
    }
    
    Bpl.Constant! GetClass(TopLevelDecl! cl)
      requires predef != null;
    {
      Bpl.Constant cc;
      if (classes.TryGetValue(cl, out cc)) {
        assert cc != null;
      } else {
        // TODO: make the following a function when the class has type parameters, so that different instantiations
        // of a class can be distinguished
        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(Token! 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 {
        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 DeclType(f) == C;
        Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass))));
        sink.TopLevelDeclarations.Add(ax);
      }
      return fc;
    }
    
    Bpl.Expr! GetField(FieldSelectExpr! fse)
      requires fse.Field != null;
    {
      return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
    }
    
    void AddFunction(Function! f)
      requires predef != null && sink != null;
    {
      Bpl.Function func;
      if (functions.TryGetValue(f, out func)) {
        assert func != null;
      } else {
        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.IsClass) {
          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);
        func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
        
        functions.Add(f, func);
        sink.TopLevelDeclarations.Add(func);
        
        if (f.IsUse) {
          Bpl.Function altF = new Bpl.Function(f.tok, f.FullName + "#alt", args, res);
          sink.TopLevelDeclarations.Add(altF);

          Bpl.Formal boolRes = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
          Bpl.Function useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes);
          sink.TopLevelDeclarations.Add(useF);
        }
      }
    }
    
    Bpl.Procedure! GetMethod(Method! m)
      requires predef != null;
    {
      Bpl.Procedure proc;
      if (methods.TryGetValue(m, out proc)) {
        assert proc != null;
      } else {
        ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
        
        Bpl.VariableSeq inParams = new Bpl.VariableSeq();
        Bpl.VariableSeq outParams = new Bpl.VariableSeq();
        if (!m.IsClass) {
          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();
        mod.Add(etran.HeapExpr);
        mod.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int));
        string comment = "user-defined preconditions";
        foreach (MaybeFreeExpression p in m.Req) {
          Bpl.RequiresSeq pieces = new Bpl.RequiresSeq();
          if (!p.IsFree) {
            foreach (Expression se in SplitExpr(p.E, true)) {
              pieces.Add(Requires(se.tok, false, etran.TrExpr(se), null, null));
            }
          }
          if (pieces.Length == 1) {
            // add 1 checked precondition (the whole thing)
            req.Add(Requires(p.E.tok, false, etran.TrExpr(p.E), null, comment));
          } else {
            // add 1 free precondition, followed by each piece (if any) as a checked precondition
            req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
            req.AddRange(pieces);
          }
          comment = null;
        }
        comment = "user-defined postconditions";
        foreach (MaybeFreeExpression p in m.Ens) {
          Bpl.EnsuresSeq pieces = new Bpl.EnsuresSeq();
          if (!p.IsFree) {
            foreach (Expression se in SplitExpr(p.E, true)) {
              pieces.Add(Ensures(se.tok, false, etran.TrExpr(se), null, null));
            }
          }
          if (pieces.Length == 1) {
            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));
            ens.AddRange(pieces);
          }
          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);
        proc = new Bpl.Procedure(m.tok, m.FullName, typeParams, inParams, outParams, req, mod, ens);
        
        methods.Add(m, proc);
      }
      return proc;
    }
    
    class BoilerplateTriple {  // a triple that is now a quintuple
      public readonly Token! tok;
      public readonly bool IsFree;
      public readonly Bpl.Expr! Expr;
      public readonly string ErrorMessage;
      invariant IsFree || ErrorMessage != null;
      public readonly string Comment;
      public BoilerplateTriple(Token! 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(Token! tok, Method! method, ExpressionTranslator! etranPre, ExpressionTranslator! etran)
    {
      List<BoilerplateTriple!> boilerplate = new List<BoilerplateTriple!>();
      
      boilerplate.Add(new BoilerplateTriple(tok, false, FrameCondition(tok, method.Mod, etranPre, etran), "frame condition does not hold", "frame condition"));

      // free specifications
      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(Token! tok, List<Expression!>! 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 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, 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.Ensures! Ensures(Token! 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(Token! 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;
        int pieces = 0;
        foreach (Expression p in SplitExpr(s.Expr, true)) {
          builder.Add(Assert(stmt.Tok, IsTotal(p, etran), "assert condition must be well defined"));  // totality check
          builder.Add(Assert(stmt.Tok, etran.TrExpr(p), "assertion violation"));
          pieces++;
        }
        if (2 <= pieces) {
          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(Assert(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;
        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 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 {
          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) {
        AddComment(builder, stmt, "call statement");
        CallStmt s = (CallStmt)stmt;
        foreach (VarDecl local in s.NewVars) {
          TrStmt(local, builder, locals, etran);
        }
        Bpl.ExprSeq ins = new Bpl.ExprSeq();
        assert s.Method != null;  // follows from the fact that stmt has been successfully resolved
        if (!s.Method.IsClass) {
          ins.Add(etran.TrExpr(s.Receiver));
        }
        for (int i = 0; i < s.Args.Count; i++) {
          Expression e = s.Args[i];
          Type t = s.Method.Ins[i].Type;
          ins.Add(etran.CondApplyBox(stmt.Tok, etran.TrExpr(e), (!)e.Type, t));
        }
        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));
          }
        }
        
        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 = s.Guard == null ? null : 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++;
        
        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?

        // 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?
        
        Bpl.Expr guard = s.Guard == null ? null : etran.TrExpr(s.Guard);
        List<Bpl.PredicateCmd!> invariants = new List<Bpl.PredicateCmd!>();
        foreach (MaybeFreeExpression loopInv in s.Invariants) {
          int pieces = 0;
          if (!loopInv.IsFree) {
            foreach (Expression se in SplitExpr(loopInv.E, true)) {
              invariants.Add(Assert(se.tok, etran.TrExpr(se), "loop invariant violation"));
              pieces++;
            }
          }
          if (pieces != 1) {
            invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
          }
        }
        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));
          }
        }
        
        // 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();
        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()));
        if (exists{Expression e in s.Decreases; e is WildcardExpr}) {
          // omit termination checking for this loop
          TrStmt(s.Body, loopBodyBuilder, locals, etran);
        } else {
          List<Bpl.Expr!> oldBfs = new List<Bpl.Expr!>();
          int c = 0;
          foreach (Expression e in s.Decreases) {
            Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, "$decr" + loopId + "$" + 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
            loopBodyBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration"));  // totality check
            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
            loopBodyBuilder.Add(cmd);
            
            c++;
          }
          // time for the actual loop body
          TrStmt(s.Body, loopBodyBuilder, locals, etran);
          // check definedness of decreases expressions
          List<Type!> types = new List<Type!>();
          List<Bpl.Expr!> decrsTotal = new List<Bpl.Expr!>();
          List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
          foreach (Expression e in s.Decreases) {
            // The following totality check implies that the loop invariant stating the same property will hold;
            // thus, an alternative (perhaps preferable) design would be:  add the totality check also just before
            // the loop, and change the loop invariant to be free.
            types.Add((!)e.Type);
            decrsTotal.Add(IsTotal(e, etran));
            decrs.Add(etran.TrExpr(e));
          }
          Bpl.Expr decrCheck = DecreasesCheck(stmt.Tok, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, "at end of loop iteration");
          loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "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 in S ==> Expr);
        // var oldHeap := $Heap;
        // havoc $Heap;
        // assume $HeapSucc(oldHeap, $Heap);
        // assume (forall o: ref, f: Field ::  $Heap[o,f] = oldHeap[o,f] || (f = F && o in S));
        // assume (forall o: ref ::  o != null && o in S ==> $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);

        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, 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)));
        }

        foreach (PredicateStmt ps in s.BodyPrefix) {
          int pieces = 0;
          if (ps is AssertStmt) {
            foreach (Expression se in SplitExpr(ps.Expr, true)) {
              Bpl.Expr e = etran.TrExpr(se);
              Bpl.Expr q = new Bpl.ForallExpr(se.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
              builder.Add(Assert(se.tok, q, "assertion violation"));
              pieces++;
            }
          }
          if (pieces != 1) {
            Bpl.Expr e;
            if (ps is UseStmt) {
              UseStmt us = (UseStmt)ps;
              e = (us.EvalInOld ? etran.Old : etran).TrUseExpr(us.FunctionCallExpr);
            } else {
              e = etran.TrExpr(ps.Expr);
            }
            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
            builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, q));
          }
        }
        
        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 in S));
        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);
        Bpl.Expr body = Bpl.Expr.Or(
          Bpl.Expr.Eq(heapOF, oldHeapOF),
          Bpl.Expr.And(
            Bpl.Expr.Eq(f, GetField((FieldSelectExpr)((!)s.BodyAssign).Lhs)),
            oInS));
        Bpl.Expr 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 ==> $Heap[o,F] =  RHS[$Heap := oldHeap]);
        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(
          Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS),
          Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(((ExprRhs)s.BodyAssign.Rhs).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 {
        assert false;  // unexpected statement
      }
    }
    
    /// <summary>
    /// Returns the expression that says whether or not the decreases function has gone down.  ee0 represents the new
    /// values and ee1 represents old values.
    /// </summary>
    Bpl.Expr! DecreasesCheck(Token! tok, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
                             Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)
      requires predef != null;
      requires types.Count == ee0.Count && ee0.Count == ee1.Count;
    {
      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, eq;
        ComputeLessEq(tok, types[i], ee0[i], ee1[i], out less, out eq, etran);
        Eq.Add(eq);
        Less.Add(less);
      }
      // check: total(ee0)
      // 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] || total0[k]
      // Also:
      // 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, and references 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]);
        }
        Bpl.Cmd cmd = Assert(ee0[k].tok, Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression (component " + k + ") must be well-defined" + suffixMsg);
        builder.Add(cmd);
        
        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]);
          }
          cmd = Assert(ee0[k].tok, Bpl.Expr.Or(bounded, Eq[k]), "decreases expression (component " + k + ") must be bounded below by 0" + suffixMsg);
          builder.Add(cmd);
        }
      }
      // check: ee0 < ee1
      Bpl.Expr decrCheck = null;
      for (int i = N; 0 <= --i; )
        invariant i != N ==> decrCheck != null;
      {
        Bpl.Expr less = Less[i];
        Bpl.Expr eq = Eq[i];
        if (decrCheck == null) {
          decrCheck = less;
        } else {
          // decrCheck = less || (eq && decrCheck)
          decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
        }
      }
      if (decrCheck == null) {
        return Bpl.Expr.False;
      } else {
        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(Token! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, 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);
      } else if (ty is IntType) {
        eq = Bpl.Expr.Eq(e0, e1);
        less = Bpl.Expr.Lt(e0, e1);
      } else if (ty is SetType) {
        eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1);
        less = etran.ProperSubset(tok, 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);
      } 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);
        
      } 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);
      }
    }
    
    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(Token! 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, 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(Token! 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 {
          FieldSelectExpr fse = (FieldSelectExpr)lhs;
          assert fse.Field != null;
          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 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
        assert lhs is IdentifierExpr;  // for this kind of RHS, the LHS is restricted to be a simple variable
        
        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);
        builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, etran.GoodRef_Class(tok, nw, (UserDefinedType)((TypeRhs)rhs).Type, true))));
        // $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(Token! 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 bool applyAltFunctions;
      
      public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! 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, bool applyAltFunctions) {
        this.translator = translator;
        this.predef = predef;
        this.HeapExpr = heap;
        this.applyAltFunctions = applyAltFunctions;
      }

      ExpressionTranslator oldEtran;
      public ExpressionTranslator! Old {
        get {
          if (oldEtran == null) {
            oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyAltFunctions);
          }
          return oldEtran;
        }
      }
      
      public ExpressionTranslator! AltFunctions {
        get {
          return new ExpressionTranslator(translator, predef, HeapExpr, true);
        }
      }

      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 = ((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 = 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 (e is UseExpr) {
            nm += "#use";
          } else if (this.applyAltFunctions && e.Function.IsUse) {
            nm += "#alt";
          }
          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.IsClass) {
            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), 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:
              return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, 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);

            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 {
          assert false;  // unexpected expression
        }
      }
      
      public Bpl.Expr! ProperSubset(Token! 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.SetEqual, null, e0, e1)));
      }
      public Bpl.Expr! ProperPrefix(Token! 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) {
        Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, ((!)e.Function).FullName + "#use", translator.TrType((!)e.Type));
        Bpl.ExprSeq args = new Bpl.ExprSeq();
        args.Add(HeapExpr);
        if (!e.Function.IsClass) {
          args.Add(TrExpr(e.Receiver));
        }
        foreach (Expression ee in e.Args) {
          args.Add(TrExpr(ee));
        }
        return new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);
      }

      public Bpl.Expr! CondApplyBox(Token! 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(Token! tok, Bpl.Expr! e, Type! fromType) {
        if (!ModeledAsBoxType(fromType)) {
          return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
        } else {
          return e;
        }
      }
      
      public Bpl.Expr! CondApplyUnbox(Token! 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(Token! 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(Token! 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(Token! tok, Bpl.Expr! e) {
        return IsAlloced(tok, e, HeapExpr);
      }
          
      Bpl.Expr! IsAlloced(Token! tok, Bpl.Expr! e, Bpl.Expr! heap) {
        return Bpl.Expr.SelectTok(tok, heap, e, predef.Alloc(tok));
      }
      
      public Bpl.Expr! GoodRef(Token! 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(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
        requires type.ResolvedClass is ClassDecl;
      {
        // 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, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)));
        r = Bpl.Expr.And(r, dtype);
        
        // dtypeParams(e, #) == T
        int n = 0;
        foreach (Type arg in type.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(Token! 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,
      
      IfThenElse,
      
      Box,
      Unbox,
      
      IsGoodHeap,
      HeapSucc,
      
      DynamicType,  // allocated type
      TypeParams,   // type parameters to allocated type
      TypeTuple,
      DeclType,
      
      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(Token! 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.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.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(Token! 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(Token! 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 IEnumerable<Expression!>! SplitExpr(Expression! expr, bool expandFunctions)
      requires expr.Type is BoolType;
    {
      if (expr is BinaryExpr) {
        BinaryExpr bin = (BinaryExpr)expr;
        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
          foreach (Expression e in SplitExpr(bin.E0, expandFunctions)) {
            yield return e;
          }
          assert bin != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
          foreach (Expression e in SplitExpr(bin.E1, expandFunctions)) {
            yield return e;
          }
          yield break;
        
        } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
          foreach (Expression e in SplitExpr(bin.E1, expandFunctions)) {
            assert bin != null;
            BinaryExpr redistributedExpr = new BinaryExpr(e.tok, bin.Op, bin.E0, e);
            redistributedExpr.ResolvedOp = bin.ResolvedOp;  redistributedExpr.Type = bin.Type;  // resolve on the fly
            yield return redistributedExpr;
          }
          yield break;
        }
      
      } else if (expr is ITEExpr) {
        ITEExpr ite = (ITEExpr)expr;
        foreach (Expression e in SplitExpr(ite.Thn, expandFunctions)) {
          assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
          BinaryExpr bin = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, ite.Test, e);
          bin.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  bin.Type = ite.Type;  // resolve on the fly
          yield return bin;
        }
        assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
        Expression negatedGuard = new UnaryExpr(ite.Test.tok, UnaryExpr.Opcode.Not, ite.Test);
        negatedGuard.Type = ite.Test.Type;  // resolve on the fly
        foreach (Expression e in SplitExpr(ite.Els, expandFunctions)) {
          assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
          assert negatedGuard != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
          BinaryExpr bin = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, negatedGuard, e);
          bin.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  bin.Type = ite.Type;  // resolve on the fly
          yield return bin;
        }
        yield break;
      
      } else if (expr is OldExpr) {
        foreach (Expression se in SplitExpr(((OldExpr)expr).E, expandFunctions)) {
          OldExpr oe = new OldExpr(expr.tok, se);
          oe.Type = se.Type;
          yield return oe;
        }
        yield break;
        
      } 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++) {
            substMap.Add(fexp.Function.Formals[i], fexp.Args[i]);
          }
          Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);
          foreach (Expression se in SplitExpr(body, false)) {
            assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that
            yield return se;
          }
          assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that
          yield break;
        }
      }
      
      yield return expr;
    }

    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;
    }
        
  }
}