fixing bug310

* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file
* default care graph computation was not sufficient, fixed

1 files changed, 9 insertions, 7 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0019b7b43..91d6beead 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -117,13 +117,13 @@ void TheoryEngine::check(Theory::Effort effort) {
     // Clear any leftover propagated equalities
     d_propagatedEqualities.clear();
 
-    // Mark the lemmas flag (no lemmas added)
-    d_lemmasAdded = false;
-
     // Mark the output channel unused (if this is FULL_EFFORT, and nothing
     // is done by the theories, no additional check will be needed)
     d_outputChannelUsed = false;
 
+    // Mark the lemmas flag (no lemmas added)
+    d_lemmasAdded = false;
+
     while (true) {
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
@@ -274,12 +274,14 @@ void TheoryEngine::combineTheories() {
 
       if (value) {
         SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory);
-        Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end());
-        d_propagatedEqualities.push_back(sharedEquality);
+        if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
+          d_propagatedEqualities.push_back(sharedEquality);
+        }
       } else {
         SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory);
-        Assert(d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end());
-        d_propagatedEqualities.push_back(sharedEquality);
+        if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
+          d_propagatedEqualities.push_back(sharedEquality);
+        }
       }
     } else {
        Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;