anchor.diff:  type Z3Constraint = GenConstraint<Z3.Expr>
   
   /// A pair of conditions.
  -type ConditionPair<'v> =
  -    {Pre: 'v 
  -     Post: 'v}
  +type ConditionPair<'v> = 
  +    { Pre : 'v
  +      Post : 'v }
   
   /// A modelled primitive command.
  -type Prim =
  -    | IntLoad of dest: Var.LValue option * src: Var.LValue * mode: Var.FetchMode
  -    | BoolLoad of dest: Var.LValue * src: Var.LValue
  -    | IntStore of dest: Var.LValue * src: Z3.ArithExpr
  -    | BoolStore of dest: Var.LValue * src: Z3.BoolExpr
  -    | IntCAS of dest: Var.LValue * test: Var.LValue * set: Z3.ArithExpr
  -    | BoolCAS of dest: Var.LValue * test: Var.LValue * set: Z3.BoolExpr
  -    | IntLocalSet of dest: Var.LValue * src: Z3.ArithExpr
  -    | BoolLocalSet of dest: Var.LValue * src: Z3.BoolExpr
  +type Prim = 
  +    | IntLoad of dest : Var.LValue option * src : Var.LValue * mode : Var.FetchMode
  +    | BoolLoad of dest : Var.LValue * src : Var.LValue
  +    | IntStore of dest : Var.LValue * src : Z3.ArithExpr
  +    | BoolStore of dest : Var.LValue * src : Z3.BoolExpr
  +    | IntCAS of dest : Var.LValue * test : Var.LValue * set : Z3.ArithExpr
  +    | BoolCAS of dest : Var.LValue * test : Var.LValue * set : Z3.BoolExpr
  +    | IntLocalSet of dest : Var.LValue * src : Z3.ArithExpr
  +    | BoolLocalSet of dest : Var.LValue * src : Z3.BoolExpr
       | PrimId
       | PrimAssume of Z3.BoolExpr
   
   /// A general Hoare triple, consisting of precondition, inner item, and
   /// postcondition.
  -type Hoare<'c, 'i> =
  -    {Conditions: ConditionPair<'c>
  -     Inner: 'i}
  +type Hoare<'c, 'i> = 
  +    { Conditions : ConditionPair<'c>
  +      Inner : 'i }
   
   type PartConditionPair = ConditionPair<Multiset<CondView>>
  +
   type PartHoare<'i> = Hoare<Multiset<CondView>, 'i>
   
   /// A flat axiom, containing a possibly-conditional Hoare triple on an
  
positive.code: type ZTerm = Hoare<Z3.BoolExpr, Z3.BoolExpr>
  
  /// A partially resolved axiom.
  type PartAxiom =
      | PAAxiom of FlatAxiom
      | PAWhile of isDo: bool * expr: Z3.BoolExpr * outer: PartConditionPair * inner: PartHoare<PartAxiom list>
      | PAITE of expr: Z3.BoolExpr * outer: PartConditionPair * inTrue: PartHoare<PartAxiom list> * inFalse: PartHoare<PartAxiom list>
  
  /// Extracts the outer condition pair of a part-axiom.
  let cpairOfPartAxiom pa =
      match pa with
      | PAAxiom a -> a.Conditions
      | PAWhile (outer = o) -> o
      | PAITE (outer = o) -> o
  
  /// A parameterised model of a Starling program.
  [<NoComparison>]
  type Model<'a, 'c> =
      {Context: Z3.Context
  
       Globals: Var.VarMap
       Locals: Var.VarMap
       Axioms: 'a
       VProtos: Map<string, (Var.Type * string) list>
  
       // This corresponds to the function D.
       DefViews: 'c}
  
  /// A partly-resolved-axiom model of a Starling program.
  type PartModel = Model<PartAxiom list, Constraint list>
  
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 }
  