Generalize atom collection in old proof code (#4626)

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.