anchor.diff:  /// Produces the reification of an unguarded view with regards to a
   /// given view definition.
   /// This corresponds to D in the theory.
  -let instantiateDef ctx model marker uview {CViews = vs; CExpr = e} =
  +let instantiateDef model marker uview {CViews = vs; CExpr = e} =
       // Make sure our view expression is actually definite.
       match e with
       | Some ee ->
  
positive.code:          * and marker.
           *)
          |> boolMarkVars marker (inSet globals)
          (* Finally, convert to Z3. *)
          |> boolToZ3 ctx
          |> ok
      | _ -> IndefiniteConstraint vs |> fail
  
  /// Produces the reification of an unguarded view multiset.
  /// This corresponds to D^ in the theory.
  let reifyZUnguarded ctx model marker uview =
      match findDefOfView model.DefViews uview with
      | Some vdef -> instantiateDef ctx model marker uview vdef
      | None -> ctx.MkTrue() |> ok
  
  let reifyZSingle (ctx: Z3.Context) model marker {Cond = c; Item = i} =
      reifyZUnguarded ctx model marker i
      |> lift (fun zv -> ctx.MkImplies(boolToZ3 ctx c, zv))
  
  /// Z3-reifies an entire view application over the given defining views.
  /// Marks the globals in the resulting expression with the given marker.
  let reifyZView (ctx: Z3.Context) model marker =
      Multiset.toSeq
      >> Seq.map (reifyZSingle ctx model marker)
      >> collect
      >> lift Seq.toArray
      >> lift (fun xs -> ctx.MkAnd xs)
  
  /// Z3-reifies all of the views in a term over the given defining model.
  let reifyZTerm ctx model term =
      (* This is also where we perform our final variable substitution,
       * converting all global variables to their pre-state in Pre, and
       * post-state in Post.
       *)
      lift2 (fun pre post ->
             { Conditions = { Pre = pre; Post = post }
               Inner = boolToZ3 ctx term.Inner })
            (reifyZView ctx model Before term.Conditions.Pre)
            (reifyZView ctx model After term.Conditions.Post)
  
  /// Reifies all of the terms in a term list.
  let reifyZ3 ctx model = tryMapAxioms (reifyZTerm ctx model) model
  
  /// Combines the components of a reified term.
  
negative.code: open Starling.Expr
  open Starling.Model
  open Starling.Reifier
  open Starling.Optimiser
  open Starling.Errors.Z3.Translator
  
  /// Converts a Starling arithmetic expression to a Z3 ArithExpr.
  