diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-22 18:19:05 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-23 01:19:05 +0000 |
| commit | 55c2f669abe354ffb258a0da89358f8c5366e2c4 (patch) | |
| tree | eb4b0e3e29f17cc24a8d57e12c6756d38ed611ef /src/expr/term_conversion_proof_generator.cpp | |
| parent | a7fe3cbb024d37b0154a779f01651afa8c0bac0b (diff) | |
BV: Add proof logging for bit-blasting. (#6373)
Diffstat (limited to 'src/expr/term_conversion_proof_generator.cpp')
| -rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 2233dcc7b..18057e149 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -133,6 +133,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t, uint32_t tctx, bool isPre) { + Assert(!t.isNull()); + Assert(!s.isNull()); + if (t == s) { return Node::null(); |