1 files changed, 2 insertions, 13 deletions
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
index f63a887ef..1467cacf3 100644
--- a/src/theory/uf/equality_engine_notify.h
+++ b/src/theory/uf/equality_engine_notify.h
@@ -33,15 +33,8 @@ class EqualityEngineNotify
   virtual ~EqualityEngineNotify(){};
 
   /**
-   * Notifies about a trigger equality that became true or false.
-   *
-   * @param equality the equality that became true or false
-   * @param value the value of the equality
-   */
-  virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0;
-
-  /**
-   * Notifies about a trigger predicate that became true or false.
+   * Notifies about a trigger predicate that became true or false. Notice that
+   * predicate can be an equality.
    *
    * @param predicate the trigger predicate that became true or false
    * @param value the value of the predicate
@@ -103,10 +96,6 @@ class EqualityEngineNotify
 class EqualityEngineNotifyNone : public EqualityEngineNotify
 {
  public:
-  bool eqNotifyTriggerEquality(TNode equality, bool value) override
-  {
-    return true;
-  }
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
   {
     return true;