anchor.diff:  module Run =
       open Starling.Core.Z3.Expr
   
  +    let genViewDefRule reals (ctx : Z3.Context) fm (fixedpoint : Z3.Fixedpoint) (unsafeapp : Z3.BoolExpr) view def =
  +        let defImpliesView =
  +            Translator.mkRule reals id ctx fm def Multiset.empty view
  +        Option.iter fixedpoint.AddRule defImpliesView
  +
  +        // TODO(CaptainHayashi): de-duplicate this with mkRule.
  +        let vars =
  +            Set.ofSeq
  +                (seq {
  +                    yield! (mapOverVars Mapper.mapBoolCtx findVars def)
  +                    for param in view.Params do
  +                        yield! (mapOverVars Mapper.mapCtx findVars param)
  +                })
  +
  +        let z3Vars =
  +            Set.toArray
  +                (Set.map
  +                    (fun (var : CTyped<Var>) ->
  +                        ctx.MkConst
  +                            (valueOf var,
  +                             Translator.typeToSort reals ctx (typeOf var)))
  +                    vars)
  +
  +        // Introduce 'V ^ ¬D(V) -> unsafe'.
  +        let viewImpliesDef =
  +            Translator.mkQuantifiedEntailment
  +                ctx
  +                z3Vars
  +                (ctx.MkAnd [| boolToZ3 reals id ctx (mkNot def)
  +                              Translator.translateVFunc reals id ctx fm view |])
  +                unsafeapp
  +        Option.iter fixedpoint.AddRule viewImpliesDef
  +
       /// <summary>
       ///     Generates a MuZ3 fixedpoint.
       /// </summary>
  
positive.code:       : Result<MuModel, Error> =
          let funcDecls, definites = translateViewDefs reals ctx ds
          let vrules = translateVariables reals ctx funcDecls svars
          let trules = xs |> Map.toSeq |> Seq.choose (translateTerm reals ctx funcDecls)
  
          let tdc = translateDeferredCheck reals ctx funcDecls svars
          let drulesResult = lift (Seq.choose id) (collect (Seq.map tdc cs))
  
negative.code:     /// </returns>
      let run (fixedpoint : Z3.Fixedpoint) (unsafe : Z3.FuncDecl) : MuSat =
          match (fixedpoint.Query [| unsafe |]) with
          | Z3.Status.SATISFIABLE -> MuSat.Sat (fixedpoint.GetAnswer ())
          | Z3.Status.UNSATISFIABLE -> MuSat.Unsat (fixedpoint.GetAnswer ())
          | Z3.Status.UNKNOWN -> MuSat.Unknown (fixedpoint.GetReasonUnknown ())
          | _ -> MuSat.Unknown "query result out of bounds"
  
  /// <summary>
  ///     The Starling MuZ3 backend driver.
  