1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c598fd01b..e55d6a9c9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -75,12 +75,18 @@ void TheoryEngine::finishInit() {
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
   d_quantEngine->addTermToDatabase( t );
+  if( d_logicInfo.isQuantified() && options::quantConflictFind() ){
+    d_quantEngine->getConflictFind()->newEqClass( t );
+  }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
   //TODO: add notification to efficient E-matching
-  if (d_logicInfo.isQuantified()) {
+  if( d_logicInfo.isQuantified() ){
     d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+    if( options::quantConflictFind() ){
+      d_quantEngine->getConflictFind()->merge( t1, t2 );
+    }
   }
 }
 
@@ -89,7 +95,11 @@ void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
 }
 
 void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-
+  if( d_logicInfo.isQuantified() ){
+    if( options::quantConflictFind() ){
+      d_quantEngine->getConflictFind()->assertDisequal( t1, t2 );
+    }
+  }
 }