anchor.diff:              (fun _ -> Seq.empty)
               mview
               m
  +    | Proof m ->
  +        printModelView
  +            (printTerm
  +                 Core.Var.Pretty.printMBoolExpr
  +                 Core.Var.Pretty.printMBoolExpr
  +                 Core.Var.Pretty.printMBoolExpr)
  +            (fun _ -> Seq.empty)
  +            mview
  +            m       
       | Z3 z -> Backends.Z3.Pretty.printResponse mview z
       | MuZ3 z -> Backends.MuZ3.Pretty.printResponse mview z
       | HSF h -> Backends.Horn.Pretty.printHorns h
  
positive.code: 
  /// Shorthand for the symbolic proof output stage.
  let symproof = bind (Core.Instantiate.Phase.run >> mapMessages Error.ModelFilterError)
  
  /// Shorthand for the HSF stage.
  let hsf = bind (Backends.Horn.hsfModel >> mapMessages Error.HSF)
  
negative.code:                  ("semantics", Request.Semantics)
                   ("termOptimise", Request.TermOptimise)
                   ("symproof", Request.SymProof)
                   ("proof", Request.Proof)
                   ("reifyZ3", Request.Z3 Backends.Z3.Types.Request.Translate)
                   ("z3", Request.Z3 Backends.Z3.Types.Request.Combine)
                   ("sat", Request.Z3 Backends.Z3.Types.Request.Sat)
  