Some incremental simplifications may be missed due to `firstNotSimplifiedFrame`

[Tomaqa]

I believe that simplifyFormulas misses simplifications when adding assertions after a pop.
In simplifyFormulas, it always starts from the frame firstNotSimplifiedFrame, but it does not distinguish whether a part of the frame was already preprocessed and another was not.

MainSolver::pop sets firstNotSimplifiedFrame as follows:

firstNotSimplifiedFrame = std::min(firstNotSimplifiedFrame, frames.frameCount());

Hence, it may later ignore simplifications in the top frame completely, because it does not use frames.frameCount() - 1.
However, if it did, it would also have to skip the simplifications it already did in a previous round.

I think the solution is to use frames.frameCount() - 1 and to also remember the size of the frame after the pop, and not traverse frame.formulas from 0, but from that position.

[Tomaqa]

Invalid: firstNotSimplifiedFrame may set to frames.frameCount() - 1 when insertFormula is called. Without that, there is no need to traverse the previous frame with nor new assertions.

Anyway, remembering the position in preprocessed formulas is implemented by #889