anchor.diff:          | Z3.Status.UNKNOWN ->
                MuSat.Unknown (fixedpoint.GetReasonUnknown ())
            | _ -> MuSat.Unknown "query result out of bounds"
  -
  -
  -/// Shorthand for the translator stage of the MuZ3 pipeline.
  -let translate = Translator.translate
  -/// Shorthand for the fixpoint generation stage of the MuZ3 pipeline.
  -let fix = Run.fixgen
  -/// Shorthand for the satisfiability stage of the MuZ3 pipeline.
  -let sat = uncurry Run.run
   
   /// <summary>
   ///     The Starling MuZ3 backend driver.
  
positive.code: /// <returns>
  ///     A function implementing the chosen MuZ3 backend process.
  /// </returns>
  let run reals req =
      use ctx = new Z3.Context()
      match req with
      | Request.Translate ->
          translate reals ctx
          >> Response.Translate
      | Request.Fix ->
          translate reals ctx
          >> fix reals ctx
          >> Response.Fix
      | Request.Sat ->
          translate reals ctx
          >> fix reals ctx
          >> sat
          >> Response.Sat
  
negative.code:     ///     implication is thrown away.
      /// </param>
      /// <returns>
      ///     An optional Z3 expression implementing the quantified implication.
      /// </returns>
      let mkQuantifiedEntailment
        (ctx : Z3.Context)
        (vars : Z3.Expr[])
        (body : Z3.BoolExpr)
        (head : Z3.BoolExpr)
        : Z3.BoolExpr option =
          (* Don't emit if the head is true: not only is the result true,
             trivial, but MuZ3 will complain about interpreted heads later.
             Also don't emit if the body is false: these are also always true. *)
  