anchor.diff:  
           mapMessages Traversal (mapper (mkTypedSub normalRec defn))
   
  +    /// <summary>Type of downclosure check results.</summary>
  +    type DownclosureResult =
  +        | /// <summary>Downclosure has been proven.</summary>
  +          Proven
  +        | /// <summary>Downclosure has been refuted.</summary>
  +          Refuted
  +        | /// <summary>Downclosure cannot be decided: reason given.</summary>
  +          Inconclusive of reason : string
  +
       /// <summary>
       ///     Runs a downclosure check using Z3.
       /// </summary>
       /// <param name="check">The check to run.</param>
       /// <returns>
  -    ///     True if <paramref name="check"/> succeeds (is a tautology);
  -    ///     false if not; an error if <paramref name="check"/> contains
  -    ///     symbols or otherwise cannot be decided by Z3.
  +    ///     The result of the downclosure check.
       /// </returns>
  -    let runDownclosureCheck (check : BoolExpr<Sym<Var>>) : Result<bool, Error> =
  +    let runDownclosureCheck (check : BoolExpr<Sym<Var>>) : DownclosureResult =
           // Expression equivalence cannot handle symbols, so try remove them.
  +        // If we can't, then we just kick downclosure down to the backend.
           // TODO(CaptainHayashi): is it sound to approximate here?
           let removeResult =
               mapTraversal
  -                (removeSymFromBoolExpr SymInIteratedConstraint)
  +                (removeSymFromBoolExpr id)
                   (mkTypedSub normalRec check)
  +        match removeResult with
           // If check is a tautology, it will be equivalent to 'true'.
  -        lift
  -            (equiv BTrue >> equivHolds id)
  -            (mapMessages Traversal removeResult)
  +        | Pass r ->
  +            if equivHolds id (equiv BTrue r) then Proven else Refuted
  +        | _ -> Inconclusive "check is symbolic"
   
       /// <summary>
       ///     Checks the base downclosure property.
  
positive.code:                The definition of emp can only mention global variables, so it
                 need not need to be freshened. *)
              let checkR = lift (mkImplies ed) baseDefnR
              let baseHoldsR = bind runDownclosureCheck checkR
              bind
                  (fun baseHolds ->
                      if baseHolds
                      then ok deferred
                      else fail (BaseDownclosureError ([func], defn, ed)))
                  baseHoldsR
  
      /// <summary>
  
negative.code:                         defn)
                  succDefnR
  
          let indHoldsR = lift runDownclosureCheck checkR
  
          bind2
              (fun succDefn indHolds ->
                  match indHolds with
                  | Proven -> ok deferred
                  | Refuted -> fail (InductiveDownclosureError ([func], succDefn, defn))
                  | Inconclusive reason ->
                      ok (NeedsInductiveDownclosure (func, reason)::deferred))
              succDefnR
              indHoldsR
  
      /// <summary>
  