diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d08405ef3..e60d60456 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -986,9 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector return changed; } -void TheoryBV::setProofLog( BitVectorProof * bvp ) { +void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) +{ if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ - d_eagerSolver->setProofLog( bvp ); + d_eagerSolver->setResolutionProofLog(bvp); }else{ for( unsigned i=0; i< d_subtheories.size(); i++ ){ d_subtheories[i]->setProofLog( bvp ); |