Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-09-14 | proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147) | Mathias Preiner | |
This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG. |