Abstraction reﬁnement is an eﬀective veriﬁcation technique for automatically proving safety properties of software. Application of this technique in shape analyses has proved impractical as core components of existing reﬁnement techniques such as backward analysis, general conjunction, and identiﬁcation of unreachable but doomed states are computationally infeasible in such domains. We propose a new method to diagnose proof failures to be used in a reﬁnement scheme for Separation Logic–based shape analyses. To check feasibility of abstract error traces, we perform Bounded Model Checking over the traces using a novel encoding into SMT. A subsequent diagnosis ﬁnds discontinuities on infeasible traces, and identiﬁes doomed states admitted by the abstraction. To construct doomed states, we give a model-ﬁnding algorithm for “symbolic heap” Separation Logic formulas, employing the execution machinery of the feasibility checker to search for concrete counter-examples. The diagnosis has been implemented in SLAyer, and we present a simple scheme for reﬁning the abstraction of hierarchical data structures, and illustrate its eﬀectiveness on benchmarks from the SLAyer test suite.