[proof] Fix open proof issues in SAT proof (#6887)

Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.

So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.

0 files changed, 0 insertions, 0 deletions