Safety property (i.e., reachability) verification is undecidable for Turing-complete programming languages. Nonetheless, recent progress has lead to heuristic verification methods, such as the ones based on predicate abstraction with counterexample-guided refinement (CEGAR), that work surprisingly well in practice. In this paper, we investigate the effectiveness of the small refinement heuristic which, for abstraction refinement in CEGAR, uses (the predicates in) a small proof of the given counterexample’s spuriousness [3,12,17,22]. Such a method has shown to be quite effective in practice but thus far lacked a theoretical backing. Our core result is that the heuristic guarantees certain bounds on the number of CEGAR iterations, relative to the size of a proof for the input program.