`TermMapper` does not track cnfized formulas

[Tomaqa]

Even though PartitionManager stores the mapping from a top-level formula to an internal, preprocessed one, mapping the formulas to the internal variables TermMapper may still be broken due to Cnfizer.
For example, formula (= x 0) is preprocessed to (and (<= x 0) (<= (- x) 0)).
However, TermMapper does not know about either of the formulas because (and (<= x 0) (<= (- x) 0)) breaks down to (<= x 0) and (<= (- x) 0) separately.
Hence, it is impossible to identify if (= x 0) or (and (<= x 0) (<= (- x) 0)) are present in the SMT solver via TermMapper::hasLit, used for example in MainSolver::getTermValue.

[Tomaqa]

One way is to disable preprocessing in Cnfizer, but that would only be feasible if we knew which formulas we potentially want to track (such as named terms); otherwise, it would be too expensive.
Another way could be to keep the simplifications but track all resulting formulas (e.g., if a conjunction is split, tracking all conjuncts).