This function causes the current set of BDDs to be replaced with the initial set of BDDs. SBSAT currently saves all of the inferences detected over the course of preprocessing. After a rewind, those saved inferences are immediately applied to the rewound set of BDDs, reducing them. This technique has been found to be useful when working with preprocessing techniques which cause BDDs to be built that are too big to be built into SMURFs. We first apply those techniques, then rewind, and then solve. This allows inferences found by the preprocessing techniques (such as clustering) to be saved and applied to the original set of BDDs, thus allowing the solver to operate on the original (manageable) functions with some reductions applied, instead of on a set of unmanageable clustered BDDs with those same reductions.