[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during double SYMM...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 12 Nov 2021 21:09:11 +0000 (15:09 -0600)
committerGitHub <noreply@github.com>
Fri, 12 Nov 2021 21:09:11 +0000 (21:09 +0000)
commit9b1c8a8053fdf57f6491ffd45be301e87e5df52e
treeb124bb6c8b6dc2bc94112a4d1503e961fd241b40
parente10051079bc5a12e23f0d87447f29f0d3c6622cb
[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during double SYMM elimination (#7630)

This fixes the potential for cyclic proofs in CDProof when P and (SYMM P) are added as proofs to a CDProof with automatic managing of symmetry.

This manifested as non-termination on the seqArray branch with proofs enabled, instead, if this were to occur, we should throw an error, which is easy to catch.
src/proof/proof.cpp
src/proof/proof_node_manager.cpp