We focus on incremental compilation-to-SAT procedures (iCTS), a promising way to push the standard CTS approaches beyond their limits. We propose the first comprehensive framework that encompasses all the aspects of an incremental decision procedure, from the encoding to the incremental solver. We apply our guidelines to a real-world CTS approach (Bounded Model Checking) and show how to modify both the generation mechanism of a real BMC tool (NuSMV) and the solving engine of a public-domain SAT solver (SIM). Related approaches and experimental results are discussed as well.