1 files changed, 2 insertions, 14 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index bccd2e943..96f82b059 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,9 +2,9 @@
 /*! \file congruence_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Paul Meng
+ **   Tim King, Mathias Preiner, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -78,12 +78,6 @@ private:
   };
   ArithCongruenceNotify d_notify;
 
-  /** module for shostak normalization, d_eqi_counter is how many pending merges
-   * in d_eq_infer we have processed */
-  std::unique_ptr<quantifiers::EqualityInference> d_eq_infer;
-  context::CDO<unsigned> d_eqi_counter;
-  Node d_true;
-
   context::CDList<Node> d_keepAlive;
 
   /** Store the propagations. */
@@ -140,9 +134,6 @@ private:
   void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
 
   Node explainInternal(TNode internal);
-
-  void eqNotifyNewClass(TNode t);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
 public:
 
   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
@@ -176,9 +167,6 @@ public:
 
 
   void addSharedTerm(Node x);
-
-  /** process inferred equalities based on Shostak normalization */
-  bool fixpointInfer();
   
   eq::EqualityEngine * getEqualityEngine() { return &d_ee; }