anchor.diff:      ///     implication is thrown away.
       /// </param>
       /// <returns>
  -    ///     A Z3 expression implementing the quantified implication.
  -    /// </returns>
  -    let mkQuantifiedEntailment (ctx : Z3.Context)
  -                               vars
  -                               (body : Z3.BoolExpr)
  -                               (head : Z3.BoolExpr) =
  +    ///     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. *)
  
positive.code:     ///     A sequence containing at most one pair of <c>string</c> and
      ///     Z3 <c>BoolExpr</c> representing the variable initialisation rule.
      /// </returns>
      let translateVariables reals ctx funcDecls svars =
          let vpars =
              svars
              |> Map.toList
  
negative.code:                printMap Inline String (fun s -> String (s.ToString())) fdm) ]
  
      /// Pretty-prints a response.
      let printResponse (mview : ModelView) : Response -> Doc =
          function
          | Response.Translate mm ->
              printMuModel mm
  