diff options
Diffstat (limited to 'src/theory/bv/bv_solver_lazy.cpp')
| -rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index ad673b402..c0f34c132 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -368,7 +368,8 @@ bool BVSolverLazy::needsCheckLastEffort() return false; } -bool BVSolverLazy::collectModelInfo(TheoryModel* m) +bool BVSolverLazy::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { Assert(!inConflict()); if (options::bitblastMode() == options::BitblastMode::EAGER) @@ -382,7 +383,7 @@ bool BVSolverLazy::collectModelInfo(TheoryModel* m) { if (d_subtheories[i]->isComplete()) { - return d_subtheories[i]->collectModelInfo(m, true); + return d_subtheories[i]->collectModelValues(m, termSet); } } return true; @@ -719,13 +720,6 @@ void BVSolverLazy::notifySharedTerm(TNode t) Debug("bitvector::sharing") << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (options::bitvectorEqualitySolver()) - { - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - d_subtheories[i]->addSharedTerm(t); - } - } } EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) |