Unsat cores only need the mapping of the reasons for the unsatisfiability to top-level formulas, not the formulas/clauses themselves needed to reconstruct the proof. Investigate how this could be optimized and also if we need to track all partitions, or just those related to the named terms (may be related to #885).
Unsat cores only need the mapping of the reasons for the unsatisfiability to top-level formulas, not the formulas/clauses themselves needed to reconstruct the proof. Investigate how this could be optimized and also if we need to track all partitions, or just those related to the named terms (may be related to #885).