diff options
| author | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
| commit | f49ddf87046793972a7f6a1bdae15003709f08d2 (patch) | |
| tree | b008e40a4e29be9455bc09a65bf2437588900104 /src/theory/bv/theory_bv.cpp | |
| parent | 4930de53415ffbf614d6965af59b1f44e405451c (diff) | |
Making the ExtTheory object a private member of Theory.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2fc5fd096..ca7c037ef 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -71,9 +71,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_extf_range_infer(u), d_extf_collapse_infer(u) { - d_extt = new ExtTheory( this ); - d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT ); - d_extt->addFunctionKind( kind::INT_TO_BITVECTOR ); + setupExtTheory(); + getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); + getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { d_eagerSolver = new EagerBitblastSolver(this); @@ -114,7 +114,6 @@ TheoryBV::~TheoryBV() { delete d_subtheories[i]; } delete d_abstractionModule; - delete d_extt; } void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { |