5 files changed, 3 insertions, 14 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 465128b1b..f2db70d90 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -477,10 +477,6 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
   d_ee->assertEquality(eq, true, reason);
 }
 
-void ArithCongruenceManager::addSharedTerm(Node x){
-  d_ee->addTriggerTerm(x, THEORY_ARITH);
-}
-
 bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
 
 std::vector<Node> andComponents(TNode an)
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 6115fec8a..44a2b9df6 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -217,9 +217,6 @@ public:
   void equalsConstant(ConstraintCP eq);
   void equalsConstant(ConstraintCP lb, ConstraintCP ub);
 
-
-  void addSharedTerm(Node x);
-
  private:
   class Statistics {
   public:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 434d2e1c8..bddc8ebcc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -219,12 +219,9 @@ void TheoryArith::propagate(Effort e) {
   d_internal->propagate(e);
 }
 
-bool TheoryArith::collectModelInfo(TheoryModel* m)
+bool TheoryArith::collectModelInfo(TheoryModel* m,
+                                   const std::set<Node>& termSet)
 {
-  std::set<Node> termSet;
-  // Work out which variables are needed
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  computeAssertedTerms(termSet, irrKinds);
   // this overrides behavior to not assert equality engine
   return collectModelValues(m, termSet);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 8555156a5..6b279c9ed 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -91,7 +91,7 @@ class TheoryArith : public Theory {
   void propagate(Effort e) override;
   TrustNode explain(TNode n) override;
 
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) override;
   /**
    * Collect model values in m based on the relevant terms given by termSet.
    */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 557072319..bb6ab0b9c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1076,7 +1076,6 @@ void TheoryArithPrivate::notifySharedTerm(TNode n)
   if(n.isConst()){
     d_partialModel.invalidateDelta();
   }
-  d_congruenceManager.addSharedTerm(n);
   if(!n.isConst() && !isSetup(n)){
     Polynomial poly = Polynomial::parsePolynomial(n);
     Polynomial::iterator it = poly.begin();