Generalize atom collection in old proof code (#4626)

Before terms in assertions that are not sent to the SAT solver could be collected by the old proof code as atoms and thus expected to have a corresponding SAT variable. This commit fixes this by making the atom collection from assertions more conservative.

1 files changed, 0 insertions, 3 deletions

diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 147835ecd..e54edd8b7 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -225,8 +225,5 @@ inline const bool getBit(Expr expr, unsigned i) {
   return (bit == 1u);
 }
 
-void collectAtoms(TNode node, std::set<Node>& seen);
-
-
 }
 }