Abstract Consistency-based diagnosis is a formal approach to software fault localization that explains failing executions by identifying program components whose modification would restore correctness. Tools such as BugAssist and (more recently) CFaults instantiate this idea using logical encodings and bounded model checking. In our first contribution, we improve on this line of work. We present SherLoc , a consistency-based diagnosis engine for ANSI-C programs with multiple failing test cases. SherLoc introduces an explicit repair model that supports pointers and arrays, ensuring that diagnoses correspond only to semantically valid C repairs. In addition, we adapt efficient algorithms from hardware diagnosis, which avoid costly self-composition, and significantly outperform existing tools on standard benchmarks. In our second contribution, we expose fundamental limitations of formal fault localization: program optimizations and transformations can invalidate diagnoses despite semantic equivalence, representing a major hurdle to further scalability improvements; function inlining can break the functional consistency of repairs, yielding diagnoses that cannot be realized at the source level; and bounded encodings inherently miss diagnoses in the presence of loops or unbounded behavior. Our exposition clarifies the gap between the formal ideal of sound and complete diagnosis and what current techniques can realistically guarantee, and thereby helps guide future work toward more robust and principled approaches.