anchor.diff:  
   /// Shorthand for the symbolic proof output stage.
   let symproof = bind (Core.Instantiate.Phase.run >> mapMessages Error.ModelFilterError)
  +
  +/// Shorthand for the non-symbolic proof output stage.
  +let proof approx v =
  +    let aprC =
  +        if approx
  +        then
  +            Starling.Core.Command.SymRemove.removeSym
  +        else id
  +
  +    let apr position =
  +        if approx
  +        then
  +            Core.TypeSystem.Mapper.mapBoolCtx
  +                Starling.Core.Symbolic.Queries.approx
  +                position
  +            >> snd
  +        else id
  +
  +    let sub = 
  +        Core.TypeSystem.Mapper.mapBoolCtx
  +            (tsfRemoveSym Core.Instantiate.Types.UnwantedSym)
  +            Core.Sub.Types.SubCtx.NoCtx
  +        >> snd
  +    
  +    let pos = Starling.Core.Sub.Position.positive
  +    let neg = Starling.Core.Sub.Position.negative
  +    
  +    bind
  +        (tryMapAxioms
  +             (tryMapTerm
  +                  (aprC >> (apr neg) >> sub)
  +                  ((apr neg) >> sub)
  +                  ((apr pos) >> sub))
  +         >> mapMessages Error.ModelFilterError)
  +        v
   
   /// Shorthand for the HSF stage.
   let hsf = bind (Backends.Horn.hsfModel >> mapMessages Error.HSF)
  
positive.code:                  ("semantics", Request.Semantics)
                   ("termOptimise", Request.TermOptimise)
                   ("symproof", Request.SymProof)
                   ("reifyZ3", Request.Z3 Backends.Z3.Types.Request.Translate)
                   ("z3", Request.Z3 Backends.Z3.Types.Request.Combine)
                   ("sat", Request.Z3 Backends.Z3.Types.Request.Sat)
  
negative.code: 
          match request with
          | Request.SymProof -> phase symproof Response.SymProof
          | Request.Proof    -> phase (symproof >> proof approx) Response.Proof
          | Request.HSF      -> phase (filterIndefinite >> hsf) Response.HSF
          | Request.Z3 rq    -> phase (maybeApprox >> filterDefinite >> z3 reals rq) Response.Z3
          | Request.MuZ3 rq  -> phase (filterIndefinite >> muz3 reals rq) Response.MuZ3
  