Many formal method tools for increasing software reliability
apply Satisfiability Modulo Theories (SMT) solvers to enumerate 
feasible paths in a program subject to certain coverage criteria. Examples
include inconsistent code detection tools and concolic test case 
generators. These tools have in common that they typically treat the SMT
solver as a black box, relying on its ability to efficiently search through
large search spaces. However, in practice the performance of SMT solvers
often degrades significantly if the search involves reasoning about 
complex control-flow. In this paper, we open the black box and devise a
new algorithm for this problem domain that we call conflict-directed
graph coverage. Our algorithm relies on two core components of an SMT
solver, namely conflict-directed learning and deduction by propagation,
and applies domain-specific modifications for reasoning about control-
flow graphs. We implemented conflict-directed coverage and used it for
detecting code inconsistencies in several large Java open-source projects
with over one million lines of code in total. The new algorithm yields 
significant performance gains on average compared to previous algorithms
and reduces the running times on hard search instances from hours to
seconds.