diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-10 10:58:35 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-10 17:58:35 +0000 |
| commit | 978f295178a2e70e16aca2ce2b951cc9afe2be40 (patch) | |
| tree | b69bbc208146674655e62a18359e91d942c2712d /src/smt/proof_post_processor.cpp | |
| parent | 9dd4f07a560c4d4b44b81bd021466966d3b494e9 (diff) | |
bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)
This PR is based on #7171
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index f5d0e8ee8..4bb875f72 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1105,7 +1105,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else if (id == PfRule::BV_BITBLAST) { - bv::BBProof bb(nullptr, d_pnm, true); + bv::BBProof bb(d_env, nullptr, d_pnm, true); Node eq = args[0]; Assert(eq.getKind() == EQUAL); bb.bbAtom(eq[0]); |