anchor.diff:  type View = GenView<Z3.Expr>
   
   /// A conditional (flat or if-then-else) view.
  -type CondView =
  +type CondView = 
       // TODO(CaptainHayashi): rename to View.
       | CITEView of Z3.BoolExpr * Multiset<CondView> * Multiset<CondView>
       // TODO(CaptainHayashi): expand to all expressions.
       | CSetView of View
   
   /// A guarded item.
  -type Guarded<'a> =
  -    {GCond: Z3.BoolExpr
  -     GItem: 'a}
  +type Guarded<'a> = 
  +    { GCond : Z3.BoolExpr
  +      GItem : 'a }
   
   /// A guarded view.
   type GuarView = Guarded<View>
  
positive.code: type SemAxiom = Hoare<Multiset<GuarView>, Z3.BoolExpr>
  
  /// An axiom combined with a frame.
  type FramedAxiom =
      {Axiom: SemAxiom
       Frame: Multiset<GuarView>}
  
  /// An unreified term.
  type Term = Hoare<Multiset<GuarView>, Z3.BoolExpr>
      
  /// A reified term.
  type ReTerm = Hoare<Multiset<ReView>, Z3.BoolExpr>
  
  
negative.code: type SemModel = Model<SemAxiom list, Constraint list>
  
  /// Disposes the Z3 context inside a Model.
  let disposeZ3 model = model.Context.Dispose()
  
  /// Creates a new model that is the input model with a different axiom set.
  /// The axiom set may be of a different type.
  let withAxioms (axioms : 'y) (model : Model<'x, 'c>) : Model<'y, 'c> = 
      { Context = model.Context
        Globals = model.Globals
        Locals = model.Locals
        VProtos = model.VProtos
        DefViews = model.DefViews
        Axioms = axioms }
  