1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 31b44aa70..869e9100e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -72,6 +72,12 @@ void TheoryModel::finishInit()
   {
     setSemiEvaluatedKind(kind::APPLY_UF);
   }
+  // Equal and not terms are not relevant terms. In other words, asserted
+  // equalities and negations of predicates (as terms) do not need to be sent
+  // to the model. Regardless, theories should send information to the model
+  // that ensures that all assertions are satisfied.
+  setIrrelevantKind(EQUAL);
+  setIrrelevantKind(NOT);
 }
 
 void TheoryModel::reset(){
@@ -627,6 +633,13 @@ void TheoryModel::setSemiEvaluatedKind(Kind k)
   d_semi_evaluated_kinds.insert(k);
 }
 
+void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); }
+
+const std::set<Kind>& TheoryModel::getIrrelevantKinds() const
+{
+  return d_irrKinds;
+}
+
 bool TheoryModel::isLegalElimination(TNode x, TNode val)
 {
   return !expr::hasSubtermKinds(d_unevaluated_kinds, val);