Detection of infeasible code has recently been identified as a
scalable and automated technique to locate likely defects in software
programs.  Given the (acyclic) control-flow graph of a procedure,
infeasible code detection depends on an exhaustive search for feasible
paths through the graph. A number of encodings of control-flow graphs
into logic (understood by theorem provers) have been proposed in the
past for this application. In this paper, we compare the performance
of these different encodings in terms of runtime and the number of
queries processed by the prover. We present a theory of acyclic
control-flow as an alternative method of handling control-flow graphs.
Such a theory can be built into theorem provers by means of theory
plug-ins.  Our experiments show that such native handling of
control-flow can lead to significant performance gains, compared to
previous encodings.