summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r--src/theory/theory.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index fa2eed861..1998498f5 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -52,11 +52,12 @@ void Theory::addSharedTermInternal(TNode n) {
}
void Theory::computeCareGraph(CareGraph& careGraph) {
- for (; d_sharedTermsIndex < d_sharedTerms.size(); d_sharedTermsIndex = d_sharedTermsIndex + 1) {
- TNode a = d_sharedTerms[d_sharedTermsIndex];
+ Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl;
+ for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
+ TNode a = d_sharedTerms[i];
TypeNode aType = a.getType();
- for (unsigned i = 0; i < d_sharedTermsIndex; ++ i) {
- TNode b = d_sharedTerms[i];
+ for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
+ TNode b = d_sharedTerms[j];
if (b.getType() != aType) {
// We don't care about the terms of different types
continue;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback