Previous implementation of handling incrementality in Preprocessor was not sound. The problem was the difference between eager push/pop and lazy application of preprocessing in MainSolver.
The lazy approach means that formulas are sent to the preprocessor only after a call to check-sat, i.e., possibly after several push commands. This meant that Preprocessor actually stored information incorrectly, because it considered all formulas processed during a check-sat command to be part of the last frame, when actually they could come from lower frames.
The proposed solution is to make tracking frames in Preprocessor lazy as well. This ensures that the frame information is stored correctly and formulas are not popped in Preprocessor when they are actually still valid in the MainSolver.
Previous implementation of handling incrementality in Preprocessor was not sound. The problem was the difference between eager push/pop and lazy application of preprocessing in MainSolver. The lazy approach means that formulas are sent to the preprocessor only after a call to check-sat, i.e., possibly after several push commands. This meant that Preprocessor actually stored information incorrectly, because it considered all formulas processed during a check-sat command to be part of the last frame, when actually they could come from lower frames.
The proposed solution is to make tracking frames in Preprocessor lazy as well. This ensures that the frame information is stored correctly and formulas are not popped in Preprocessor when they are actually still valid in the MainSolver.
Fixes #710.