anchor.diff:          printUFModelView (printSTerm printSMGView printSMVFunc) mview m
       | TermOptimise m ->
           printUFModelView (printSTerm printSMGView printSMVFunc) mview m
  -    | Proof m ->
  +    | SymProof m ->
           printModelView
               (printTerm printSMBoolExpr printSMBoolExpr printSMBoolExpr)
               (fun _ -> Seq.empty)
  
positive.code: let printResult pOk pBad =
      either (printOk pOk pBad) (printErr pBad)
  
  /// Shorthand for the proof-output stage.
  let proof = bind (Core.Instantiate.Phase.run >> mapMessages Error.ModelFilterError)
  
  /// Shorthand for the HSF stage.
  let hsf = bind (Backends.Horn.hsfModel >> mapMessages Error.HSF)
  
negative.code:                  else id)
  
          match request with
          | Request.SymProof -> phase symproof Response.SymProof
          | 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
          | _                -> fail (Error.Other "Internal")
  
      //Build a phase with
      //  op as what to do
  