1 files changed, 14 insertions, 9 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 045af0864..c539315af 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -78,24 +78,26 @@ void TheoryEngine::finishInit() {
 }
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
-  if( d_logicInfo.isQuantified() ){
-    d_quantEngine->addTermToDatabase( t );
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyNewClass( t );
   }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyPreMerge( t1, t2 );
+  }
 }
 
 void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyPostMerge( t1, t2 );
+  }
 }
 
 void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-  if( d_logicInfo.isQuantified() ){
-    if( options::quantConflictFind() ){
-      d_quantEngine->getConflictFind()->assertDisequal( t1, t2 );
-    }
+  if (d_logicInfo.isQuantified()) {
+    d_quantEngine->eqNotifyDisequal( t1, t2, reason );
   }
 }
 
@@ -405,6 +407,9 @@ void TheoryEngine::check(Theory::Effort effort) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
         combineTheories();
+        if(d_logicInfo.isQuantified()){
+          d_quantEngine->notifyCombineTheories();
+        }
       }
     }
 
@@ -419,7 +424,7 @@ void TheoryEngine::check(Theory::Effort effort) {
         // must build model at this point
         d_curr_model_builder->buildModel(d_curr_model, true);
       }
-    Trace("theory::assertions-model") << endl;
+      Trace("theory::assertions-model") << endl;
       if (Trace.isOn("theory::assertions-model")) {
         printAssertions("theory::assertions-model");
       }