In the past few years, general-purpose propositional satisfiability (SAT) solvers
have improved dramatically in performance and have been used to tackle many new
problems.  It has also been shown that certain simple fragments of
first-order logic can be decided efficiently by first translating
the problem into an equivalent SAT problem and then using a fast SAT solver.
In this paper, we describe an alternative but similar approach to using SAT in
conjunction with a more expressive fragment of first-order logic.  However, rather than
translating the entire formula up front, the formula is incrementally
translated during a search for the solution.  As a result, only that portion of
the translation that is actually relevant to the solution is obtained.  We describe
a number of obstacles that had to be overcome before developing an approach which was ultimately
very effective, and give results on verification benchmarks using CVC (Cooperating Validity
Checker), which includes the Chaff SAT solver.  The results show a performance
gain of several orders of magnitude over CVC without Chaff and indicate that the method
is more robust than the heuristics found in CVC's predecessor, SVC.