Cleanup of inferences in arithmetic theory (#5927)

This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:

    remove the ArithLemma class and uses SimpleTheoryLemma instead
    only use NlLemma if we actually need it
    use proper InferenceIds everywhere
    remove unused code in the nonlinear extension

25 files changed, 152 insertions, 288 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 96f98bd4c..3bfb248a4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -291,8 +291,6 @@ libcvc4_add_sources(
   theory/arith/approx_simplex.h
   theory/arith/arith_ite_utils.cpp
   theory/arith/arith_ite_utils.h
-  theory/arith/arith_lemma.cpp
-  theory/arith/arith_lemma.h
   theory/arith/arith_msum.cpp
   theory/arith/arith_msum.h
   theory/arith/arith_preprocess.cpp
diff --git a/src/theory/arith/arith_lemma.cpp b/src/theory/arith/arith_lemma.cpp
deleted file mode 100644
index 9b8222586..000000000
--- a/src/theory/arith/arith_lemma.cpp
+++ /dev/null
@@ -1,28 +0,0 @@
-/*********************                                                        */
-/*! \file arith_lemma.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer
- ** This file is part of the CVC4 project.
- ** 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
- **
- ** \brief ArithLemma class, derived from Lemma.
- **/
-
-#include "theory/arith/arith_lemma.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-std::ostream& operator<<(std::ostream& out, const ArithLemma& al)
-{
-  return out << al.d_node;
-}
-
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h
deleted file mode 100644
index e50df15c0..000000000
--- a/src/theory/arith/arith_lemma.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file arith_lemma.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer
- ** This file is part of the CVC4 project.
- ** 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
- **
- ** \brief ArithLemma class, derived from Lemma.
- **/
-
-#ifndef CVC4__THEORY__ARITH__ARITH_LEMMA_H
-#define CVC4__THEORY__ARITH__ARITH_LEMMA_H
-
-#include <tuple>
-#include <vector>
-
-#include "expr/node.h"
-#include "theory/inference_id.h"
-#include "theory/inference_manager_buffered.h"
-#include "theory/output_channel.h"
-#include "theory/theory_inference.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-/**
- * The data structure for a single lemma to process by the arithmetic theory,
- * derived from theory::SimpleTheoryLemma.
- *
- * This also includes the inference type that produced this lemma.
- */
-class ArithLemma : public SimpleTheoryLemma
-{
- public:
-  ArithLemma(Node n,
-             LemmaProperty p,
-             ProofGenerator* pg,
-             InferenceId inf = InferenceId::UNKNOWN)
-      : SimpleTheoryLemma(inf, n, p, pg)
-  {
-  }
-  virtual ~ArithLemma() {}
-};
-/**
- * Writes an arithmetic lemma to a stream.
- */
-std::ostream& operator<<(std::ostream& out, const ArithLemma& al);
-
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__ARITH__ARITH_LEMMA_H */
diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 80217195f..3e0937e8b 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom)
   // tn is of kind REWRITE, turn this into a LEMMA here
   TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
   // must preprocess
-  d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
+  d_im.trustedLemma(tlem, InferenceId::ARITH_PP_ELIM_OPERATORS);
   // mark the atom as reduced
   d_reduced[atom] = true;
   return true;
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index c406c0ce6..c2001686b 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -29,8 +29,8 @@ InferenceManager::InferenceManager(TheoryArith& ta,
 {
 }
 
-void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
-                                            bool isWaiting)
+void InferenceManager::addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
+                                       bool isWaiting)
 {
   Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node
                          << (isWaiting ? " as waiting" : "") << std::endl;
@@ -59,21 +59,22 @@ void InferenceManager::addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
     d_pendingLem.emplace_back(std::move(lemma));
   }
 }
-void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
-                                            bool isWaiting)
+void InferenceManager::addPendingLemma(const SimpleTheoryLemma& lemma,
+                                       bool isWaiting)
 {
-  addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(lemma)),
-                       isWaiting);
+  addPendingLemma(
+      std::unique_ptr<SimpleTheoryLemma>(new SimpleTheoryLemma(lemma)),
+      isWaiting);
 }
-void InferenceManager::addPendingArithLemma(const Node& lemma,
-                                            InferenceId inftype,
-                                            ProofGenerator* pg,
-                                            bool isWaiting,
-                                            LemmaProperty p)
+void InferenceManager::addPendingLemma(const Node& lemma,
+                                       InferenceId inftype,
+                                       ProofGenerator* pg,
+                                       bool isWaiting,
+                                       LemmaProperty p)
 {
-  addPendingArithLemma(
-      std::unique_ptr<ArithLemma>(new ArithLemma(lemma, p, pg, inftype)),
-      isWaiting);
+  addPendingLemma(std::unique_ptr<SimpleTheoryLemma>(
+                      new SimpleTheoryLemma(inftype, lemma, p, pg)),
+                  isWaiting);
 }
 
 void InferenceManager::flushWaitingLemmas()
@@ -119,7 +120,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
   return TheoryInferenceManager::cacheLemma(rewritten, p);
 }
 
-bool InferenceManager::isEntailedFalse(const ArithLemma& lem)
+bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
 {
   if (options::nlExtEntailConflicts())
   {
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index ea3e1850a..f033c4a5c 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -20,7 +20,6 @@
 #include <map>
 #include <vector>
 
-#include "theory/arith/arith_lemma.h"
 #include "theory/arith/arith_state.h"
 #include "theory/inference_id.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
@@ -55,24 +54,24 @@ class InferenceManager : public InferenceManagerBuffered
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
-  void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma,
-                            bool isWaiting = false);
+  void addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
+                       bool isWaiting = false);
   /**
    * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
-  void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false);
+  void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false);
   /**
    * Add a lemma as pending lemma to this inference manager.
    * If isWaiting is true, the lemma is first stored as waiting lemma and only
    * added as pending lemma when calling flushWaitingLemmas.
    */
-  void addPendingArithLemma(const Node& lemma,
-                            InferenceId inftype,
-                            ProofGenerator* pg = nullptr,
-                            bool isWaiting = false,
-                            LemmaProperty p = LemmaProperty::NONE);
+  void addPendingLemma(const Node& lemma,
+                       InferenceId inftype,
+                       ProofGenerator* pg = nullptr,
+                       bool isWaiting = false,
+                       LemmaProperty p = LemmaProperty::NONE);
 
   /**
    * Flush all waiting lemmas to this inference manager (as pending
@@ -112,10 +111,10 @@ class InferenceManager : public InferenceManagerBuffered
    * Checks whether the lemma is entailed to be false. In this case, it is a
    * conflict.
    */
-  bool isEntailedFalse(const ArithLemma& lem);
+  bool isEntailedFalse(const SimpleTheoryLemma& lem);
 
   /** The waiting lemmas. */
-  std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
+  std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem;
 };
 
 }  // namespace arith
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 5418ea5bb..83ceb1182 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -92,8 +92,8 @@ void CadSolver::checkFull()
     {
       n = n.negate();
     }
-    d_im.addPendingArithLemma(NodeManager::currentNM()->mkOr(mis),
-                              InferenceId::ARITH_NL_CAD_CONFLICT);
+    d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis),
+                         InferenceId::ARITH_NL_CAD_CONFLICT);
   }
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
@@ -140,7 +140,8 @@ void CadSolver::checkPartial()
         Trace("nl-cad") << "Excluding " << first_var << " -> "
                         << interval.d_interval << " using " << lemma
                         << std::endl;
-        d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL);
+        d_im.addPendingLemma(lemma,
+                             InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL);
       }
     }
   }
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 20f89aa82..7b4d98037 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -167,7 +167,7 @@ void FactoringCheck::check(const std::vector<Node>& asserts,
             proof->addStep(
                 flem, PfRule::MACRO_SR_PRED_TRANSFORM, {split, k_eq}, {flem});
           }
-          d_data->d_im.addPendingArithLemma(
+          d_data->d_im.addPendingLemma(
               flem, InferenceId::ARITH_NL_FACTOR, proof);
         }
       }
@@ -186,7 +186,7 @@ Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof)
     Node k_eq = k.eqNode(n);
     Trace("nl-ext-factor") << "...adding factor skolem " << k << " == " << n
                            << std::endl;
-    d_data->d_im.addPendingArithLemma(k_eq, InferenceId::ARITH_NL_FACTOR, proof);
+    d_data->d_im.addPendingLemma(k_eq, InferenceId::ARITH_NL_FACTOR, proof);
     d_factor_skolem[n] = k;
   }
   else
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 9ffaf53c1..46b1c991e 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -319,8 +319,10 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
                 << " (pre-rewrite : " << pr_iblem << ")" << std::endl;
             // Trace("nl-ext-bound-lemma") << "       intro new
             // monomials = " << introNewTerms << std::endl;
-            d_data->d_im.addPendingArithLemma(
-                iblem, InferenceId::ARITH_NL_INFER_BOUNDS_NT, nullptr, introNewTerms);
+            d_data->d_im.addPendingLemma(iblem,
+                                         InferenceId::ARITH_NL_INFER_BOUNDS_NT,
+                                         nullptr,
+                                         introNewTerms);
           }
         }
       }
@@ -478,7 +480,7 @@ void MonomialBoundsCheck::checkResBounds()
                   rblem = Rewriter::rewrite(rblem);
                   Trace("nl-ext-rbound-lemma")
                       << "Resolution bound lemma : " << rblem << std::endl;
-                  d_data->d_im.addPendingArithLemma(
+                  d_data->d_im.addPendingLemma(
                       rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS);
                 }
               }
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index a007dd4a6..c6ee3d764 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -112,7 +112,7 @@ void MonomialCheck::checkMagnitude(unsigned c)
   }
 
   unsigned r = 1;
-  std::vector<ArithLemma> lemmas;
+  std::vector<SimpleTheoryLemma> lemmas;
   // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
   // in lemmas
   std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
@@ -274,7 +274,7 @@ void MonomialCheck::checkMagnitude(unsigned c)
   {
     if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end())
     {
-      d_data->d_im.addPendingArithLemma(lemmas[i]);
+      d_data->d_im.addPendingLemma(lemmas[i]);
     }
   }
   // could only take maximal lower/minimial lower bounds?
@@ -295,7 +295,7 @@ int MonomialCheck::compareSign(
     {
       Node lemma =
           nm->mkAnd(exp).impNode(mkLit(oa, d_data->d_zero, status * 2));
-      d_data->d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_SIGN);
+      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN);
     }
     return status;
   }
@@ -321,7 +321,7 @@ int MonomialCheck::compareSign(
         proof->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {prem}, {conc});
         proof->addStep(lemma, PfRule::SCOPE, {conc}, {prem});
       }
-      d_data->d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_SIGN, proof);
+      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN, proof);
     }
     return 0;
   }
@@ -342,7 +342,7 @@ bool MonomialCheck::compareMonomial(
     Node b,
     NodeMultiset& b_exp_proc,
     std::vector<Node>& exp,
-    std::vector<ArithLemma>& lem,
+    std::vector<SimpleTheoryLemma>& lem,
     std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
 {
   Trace("nl-ext-comp-debug")
@@ -377,7 +377,7 @@ bool MonomialCheck::compareMonomial(
     NodeMultiset& b_exp_proc,
     int status,
     std::vector<Node>& exp,
-    std::vector<ArithLemma>& lem,
+    std::vector<SimpleTheoryLemma>& lem,
     std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
 {
   Trace("nl-ext-comp-debug")
@@ -410,7 +410,7 @@ bool MonomialCheck::compareMonomial(
           Kind::IMPLIES, nm->mkAnd(exp), mkLit(oa, ob, status, true));
       Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
       lem.emplace_back(
-          clem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_COMPARISON);
+          InferenceId::ARITH_NL_COMPARISON, clem, LemmaProperty::NONE, nullptr);
       cmp_infers[status][oa][ob] = clem;
     }
     return true;
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index ed8639ef2..51179826a 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -136,7 +136,7 @@ class MonomialCheck
       Node b,
       NodeMultiset& b_exp_proc,
       std::vector<Node>& exp,
-      std::vector<ArithLemma>& lem,
+      std::vector<SimpleTheoryLemma>& lem,
       std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
   /** helper function for above
    *
@@ -154,7 +154,7 @@ class MonomialCheck
       NodeMultiset& b_exp_proc,
       int status,
       std::vector<Node>& exp,
-      std::vector<ArithLemma>& lem,
+      std::vector<SimpleTheoryLemma>& lem,
       std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
   /** Check whether we have already inferred a relationship between monomials
    * x and y based on the information in cmp_infers. This computes the
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 2e3cb3cd1..1e9b444e3 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -45,7 +45,8 @@ void SplitZeroCheck::check()
         proof->addStep(lem, PfRule::SPLIT, {}, {eq});
       }
       d_data->d_im.addPendingPhaseRequirement(eq, true);
-      d_data->d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_SPLIT_ZERO, proof);
+      d_data->d_im.addPendingLemma(
+          lem, InferenceId::ARITH_NL_SPLIT_ZERO, proof);
     }
   }
 }
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index a4642b73a..3d646a684 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -146,8 +146,10 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
                                 b_v,
                                 nm->mkConst(Rational(d == 0 ? -1 : 1))});
               }
-              d_data->d_im.addPendingArithLemma(
-                  tlem, InferenceId::ARITH_NL_TANGENT_PLANE, proof, asWaitingLemmas);
+              d_data->d_im.addPendingLemma(tlem,
+                                           InferenceId::ARITH_NL_TANGENT_PLANE,
+                                           proof,
+                                           asWaitingLemmas);
             }
           }
         }
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index ff51f7bb5..78ffb3c09 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -99,7 +99,7 @@ void IAndSolver::checkInitialRefine()
       Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
       Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
                           << std::endl;
-      d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE);
+      d_im.addPendingLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE);
     }
   }
 }
@@ -152,7 +152,7 @@ void IAndSolver::checkFullRefine()
             << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl;
         // note that lemma can contain div/mod, and will be preprocessed in the
         // prop engine
-        d_im.addPendingArithLemma(
+        d_im.addPendingLemma(
             lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true);
       }
       else if (options::iandMode() == options::IandMode::BITWISE)
@@ -162,7 +162,7 @@ void IAndSolver::checkFullRefine()
             << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl;
         // note that lemma can contain div/mod, and will be preprocessed in the
         // prop engine
-        d_im.addPendingArithLemma(
+        d_im.addPendingLemma(
             lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true);
       }
       else
@@ -172,11 +172,11 @@ void IAndSolver::checkFullRefine()
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
         // value lemmas should not contain div/mod so we don't need to tag it with PREPROCESS
-        d_im.addPendingArithLemma(lem,
-                                  InferenceId::ARITH_NL_IAND_VALUE_REFINE,
-                                  nullptr,
-                                  true,
-                                  LemmaProperty::NONE);
+        d_im.addPendingLemma(lem,
+                             InferenceId::ARITH_NL_IAND_VALUE_REFINE,
+                             nullptr,
+                             true,
+                             LemmaProperty::NONE);
       }
     }
   }
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index af6093be1..af86d69fd 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -348,8 +348,8 @@ void ICPSolver::check()
         {
           mis.emplace_back(n.negate());
         }
-        d_im.addPendingArithLemma(NodeManager::currentNM()->mkOr(mis),
-                                  InferenceId::ARITH_NL_ICP_CONFLICT);
+        d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis),
+                             InferenceId::ARITH_NL_ICP_CONFLICT);
         did_progress = true;
         progress = false;
         break;
@@ -360,7 +360,7 @@ void ICPSolver::check()
     std::vector<Node> lemmas = generateLemmas();
     for (const auto& l : lemmas)
     {
-      d_im.addPendingArithLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION);
+      d_im.addPendingLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION);
     }
   }
 }
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index 8ae5ecc4b..7cb1da728 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -24,7 +24,7 @@ namespace nl {
 
 bool NlLemma::process(TheoryInferenceManager* im, bool asLemma)
 {
-  bool res = ArithLemma::process(im, asLemma);
+  bool res = SimpleTheoryLemma::process(im, asLemma);
   if (d_nlext != nullptr)
   {
     d_nlext->processSideEffect(*this);
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 24302339c..277751fe8 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -19,8 +19,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/arith_lemma.h"
-#include "theory/output_channel.h"
+#include "theory/theory_inference.h"
 
 namespace CVC4 {
 namespace theory {
@@ -41,18 +40,14 @@ class NonlinearExtension;
  * - A set of secant points to record (for transcendental secant plane
  * inferences).
  */
-class NlLemma : public ArithLemma
+class NlLemma : public SimpleTheoryLemma
 {
  public:
-  NlLemma(Node n,
-          LemmaProperty p,
-          ProofGenerator* pg,
-          InferenceId inf = InferenceId::UNKNOWN)
-      : ArithLemma(n, p, pg, inf)
-  {
-  }
-  NlLemma(Node n, InferenceId inf = InferenceId::UNKNOWN)
-      : ArithLemma(n, LemmaProperty::NONE, nullptr, inf)
+  NlLemma(InferenceId inf,
+          Node n,
+          LemmaProperty p = LemmaProperty::NONE,
+          ProofGenerator* pg = nullptr)
+      : SimpleTheoryLemma(inf, n, p, pg)
   {
   }
   ~NlLemma() {}
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 79f2a2350..5c4140430 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -640,7 +640,7 @@ bool NlModel::solveEqualitySimple(Node eq,
     Node conf = seq.negate();
     Trace("nl-ext-lemma") << "NlModel::Lemma : quadratic no root : " << conf
                           << std::endl;
-    lemmas.push_back(conf);
+    lemmas.emplace_back(InferenceId::ARITH_NL_CM_QUADRATIC_EQ, conf);
     Trace("nl-ext-cms") << "...fail due to negative discriminant." << std::endl;
     return false;
   }
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 36ddecee9..4d29f1955 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -106,63 +106,6 @@ void NonlinearExtension::computeRelevantAssertions(
                       << " assertions" << std::endl;
 }
 
-unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
-{
-  Trace("nl-ext-lemma-debug")
-      << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl;
-  lem.d_node = Rewriter::rewrite(lem.d_node);
-
-  if (d_im.hasCachedLemma(lem.d_node, lem.d_property))
-  {
-    Trace("nl-ext-lemma-debug")
-        << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl;
-    return 0;
-  }
-  out.emplace_back(lem);
-  return 1;
-}
-
-unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
-                                          std::vector<NlLemma>& out)
-{
-  if (options::nlExtEntailConflicts())
-  {
-    // check if any are entailed to be false
-    for (const NlLemma& lem : lemmas)
-    {
-      Node ch_lemma = lem.d_node.negate();
-      ch_lemma = Rewriter::rewrite(ch_lemma);
-      Trace("nl-ext-et-debug")
-          << "Check entailment of " << ch_lemma << "..." << std::endl;
-      std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck(
-          options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
-      Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " "
-                               << et.second << std::endl;
-      if (et.first)
-      {
-        Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
-                           << lem.d_node << std::endl;
-        // return just this lemma
-        if (filterLemma(lem, out) > 0)
-        {
-          lemmas.clear();
-          return 1;
-        }
-      }
-    }
-  }
-
-  unsigned sum = 0;
-  for (const NlLemma& lem : lemmas)
-  {
-    sum += filterLemma(lem, out);
-    d_containing.getOutputChannel().spendResource(
-        ResourceManager::Resource::ArithNlLemmaStep);
-  }
-  lemmas.clear();
-  return sum;
-}
-
 void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 {
   Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl;
@@ -293,7 +236,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions)
   bool ret = d_model.checkModel(passertions, tdegree, lemmas);
   for (const auto& al: lemmas)
   {
-    d_im.addPendingArithLemma(al);
+    d_im.addPendingLemma(al);
   }
   return ret;
 }
@@ -500,8 +443,10 @@ bool NonlinearExtension::modelBasedRefinement()
             d_containing.getOutputChannel().requirePhase(literal, true);
             Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
             Node split = literal.orNode(literal.negate());
-            NlLemma nsplit(split, InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT);
-            d_im.addPendingArithLemma(nsplit, true);
+            d_im.addPendingLemma(split,
+                                 InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT,
+                                 nullptr,
+                                 true);
           }
           if (d_im.hasWaitingLemma())
           {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index a6b68d644..fba9e8e87 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -193,15 +193,6 @@ class NonlinearExtension
   /** compute relevant assertions */
   void computeRelevantAssertions(const std::vector<Node>& assertions,
                                  std::vector<Node>& keep);
-  /**
-   * Potentially adds lemmas to the set out and clears lemmas. Returns
-   * the number of lemmas added to out. We do not add lemmas that have already
-   * been sent on the output channel of TheoryArith.
-   */
-  unsigned filterLemmas(std::vector<NlLemma>& lemmas,
-                        std::vector<NlLemma>& out);
-  /** singleton version of above */
-  unsigned filterLemma(NlLemma lem, std::vector<NlLemma>& out);
 
   /** run check strategy
    *
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index cc60d20fd..7f9d98fe1 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -45,8 +45,7 @@ void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y)
   // note we must do preprocess on this lemma
   Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                         << std::endl;
-  NlLemma nlem(lem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_T_PURIFY_ARG);
-  d_data->d_im.addPendingArithLemma(nlem);
+  d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG);
 }
 
 void ExponentialSolver::checkInitialRefine()
@@ -71,7 +70,7 @@ void ExponentialSolver::checkInitialRefine()
         {
           // exp is always positive: exp(t) > 0
           Node lem = nm->mkNode(Kind::GT, t, d_data->d_zero);
-          d_data->d_im.addPendingArithLemma(
+          d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr);
         }
         {
@@ -79,7 +78,7 @@ void ExponentialSolver::checkInitialRefine()
           Node lem = nm->mkNode(Kind::EQUAL,
                                 t[0].eqNode(d_data->d_zero),
                                 t.eqNode(d_data->d_one));
-          d_data->d_im.addPendingArithLemma(
+          d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr);
         }
         {
@@ -87,7 +86,7 @@ void ExponentialSolver::checkInitialRefine()
           Node lem = nm->mkNode(Kind::EQUAL,
                                 nm->mkNode(Kind::LT, t[0], d_data->d_zero),
                                 nm->mkNode(Kind::LT, t, d_data->d_one));
-          d_data->d_im.addPendingArithLemma(
+          d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr);
         }
         {
@@ -97,7 +96,7 @@ void ExponentialSolver::checkInitialRefine()
               nm->mkNode(Kind::LEQ, t[0], d_data->d_zero),
               nm->mkNode(
                   Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one)));
-          d_data->d_im.addPendingArithLemma(
+          d_data->d_im.addPendingLemma(
               lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr);
         }
       }
@@ -162,8 +161,8 @@ void ExponentialSolver::checkMonotonic()
                                  nm->mkNode(Kind::GEQ, t, s));
       Trace("nl-ext-exp") << "Monotonicity lemma : " << mono_lem << std::endl;
 
-      d_data->d_im.addPendingArithLemma(mono_lem,
-                                        InferenceId::ARITH_NL_T_MONOTONICITY);
+      d_data->d_im.addPendingLemma(mono_lem,
+                                   InferenceId::ARITH_NL_T_MONOTONICITY);
     }
     // store the previous values
     targ = sarg;
@@ -190,7 +189,8 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx)
   Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
-  d_data->d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true);
+  d_data->d_im.addPendingLemma(
+      lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true);
 }
 
 void ExponentialSolver::doSecantLemmas(TNode e,
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 99bb093bb..0cca238b0 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -79,8 +79,7 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
   // note we must do preprocess on this lemma
   Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                         << std::endl;
-  NlLemma nlem(lem, LemmaProperty::NONE, proof, InferenceId::ARITH_NL_T_PURIFY_ARG);
-  d_data->d_im.addPendingArithLemma(nlem);
+  d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG, proof);
 }
 
 void SineSolver::checkInitialRefine()
@@ -115,14 +114,14 @@ void SineSolver::checkInitialRefine()
           Node lem = nm->mkNode(Kind::AND,
                                 nm->mkNode(Kind::LEQ, t, d_data->d_one),
                                 nm->mkNode(Kind::GEQ, t, d_data->d_neg_one));
-          d_data->d_im.addPendingArithLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE);
+          d_data->d_im.addPendingLemma(lem,
+                                       InferenceId::ARITH_NL_T_INIT_REFINE);
         }
         {
           // sine symmetry: sin(t) - sin(-t) = 0
           Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero);
-          d_data->d_im.addPendingArithLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE);
+          d_data->d_im.addPendingLemma(lem,
+                                       InferenceId::ARITH_NL_T_INIT_REFINE);
         }
         {
           // sine zero tangent:
@@ -136,8 +135,8 @@ void SineSolver::checkInitialRefine()
                          nm->mkNode(Kind::IMPLIES,
                                     nm->mkNode(Kind::LT, t[0], d_data->d_zero),
                                     nm->mkNode(Kind::GT, t, t[0])));
-          d_data->d_im.addPendingArithLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE);
+          d_data->d_im.addPendingLemma(lem,
+                                       InferenceId::ARITH_NL_T_INIT_REFINE);
         }
         {
           // sine pi tangent:
@@ -157,8 +156,8 @@ void SineSolver::checkInitialRefine()
                   nm->mkNode(Kind::LT,
                              t,
                              nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
-          d_data->d_im.addPendingArithLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE);
+          d_data->d_im.addPendingLemma(lem,
+                                       InferenceId::ARITH_NL_T_INIT_REFINE);
         }
         {
           Node lem =
@@ -171,8 +170,8 @@ void SineSolver::checkInitialRefine()
                          nm->mkNode(Kind::EQUAL,
                                     nm->mkNode(Kind::GT, t[0], d_data->d_zero),
                                     nm->mkNode(Kind::GT, t, d_data->d_zero)));
-          d_data->d_im.addPendingArithLemma(
-              lem, InferenceId::ARITH_NL_T_INIT_REFINE);
+          d_data->d_im.addPendingLemma(lem,
+                                       InferenceId::ARITH_NL_T_INIT_REFINE);
         }
       }
     }
@@ -311,8 +310,8 @@ void SineSolver::checkMonotonic()
         Trace("nl-ext-tf-mono")
             << "Monotonicity lemma : " << mono_lem << std::endl;
 
-        d_data->d_im.addPendingArithLemma(mono_lem,
-                                          InferenceId::ARITH_NL_T_MONOTONICITY);
+        d_data->d_im.addPendingLemma(mono_lem,
+                                     InferenceId::ARITH_NL_T_MONOTONICITY);
       }
     }
     // store the previous values
@@ -352,7 +351,7 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
   Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
   Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
   // Figure 3 : line 9
-  d_data->d_im.addPendingArithLemma(
+  d_data->d_im.addPendingLemma(
       lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true);
 }
 
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 032cf1411..35967a39a 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -179,7 +179,7 @@ void TranscendentalState::ensureCongruence(TNode a,
       }
       Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
       Node cong_lemma = expn.impNode(a.eqNode(aa));
-      d_im.addPendingArithLemma(cong_lemma, InferenceId::ARITH_NL_CONGRUENCE);
+      d_im.addPendingLemma(cong_lemma, InferenceId::ARITH_NL_CONGRUENCE);
     }
   }
   else
@@ -222,7 +222,7 @@ void TranscendentalState::getCurrentPiBounds()
     proof->addStep(
         pi_lem, PfRule::ARITH_TRANS_PI, {}, {d_pi_bound[0], d_pi_bound[1]});
   }
-  d_im.addPendingArithLemma(pi_lem, InferenceId::ARITH_NL_T_PI_BOUND, proof);
+  d_im.addPendingLemma(pi_lem, InferenceId::ARITH_NL_T_PI_BOUND, proof);
 }
 
 std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
@@ -319,7 +319,7 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower,
   lem = Rewriter::rewrite(lem);
   Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
   Assert(d_model.computeAbstractModelValue(lem) == d_false);
-  return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_T_SECANT);
+  return NlLemma(InferenceId::ARITH_NL_T_SECANT, lem);
 }
 
 void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
@@ -352,7 +352,7 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
     nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
-    d_im.addPendingArithLemma(nlem, true);
+    d_im.addPendingLemma(nlem, true);
   }
 
   // take the model value of upper (since may contain PI)
@@ -371,7 +371,7 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
     nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
-    d_im.addPendingArithLemma(nlem, true);
+    d_im.addPendingLemma(nlem, true);
   }
 }
 
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index cb15b4326..0268fa31a 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -21,30 +21,42 @@ const char* toString(InferenceId i)
 {
   switch (i)
   {
-    case InferenceId::ARITH_NL_CONGRUENCE: return "CONGRUENCE";
-    case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT";
-    case InferenceId::ARITH_NL_SPLIT_ZERO: return "SPLIT_ZERO";
-    case InferenceId::ARITH_NL_SIGN: return "SIGN";
-    case InferenceId::ARITH_NL_COMPARISON: return "COMPARISON";
-    case InferenceId::ARITH_NL_INFER_BOUNDS: return "INFER_BOUNDS";
-    case InferenceId::ARITH_NL_INFER_BOUNDS_NT: return "INFER_BOUNDS_NT";
-    case InferenceId::ARITH_NL_FACTOR: return "FACTOR";
-    case InferenceId::ARITH_NL_RES_INFER_BOUNDS: return "RES_INFER_BOUNDS";
-    case InferenceId::ARITH_NL_TANGENT_PLANE: return "TANGENT_PLANE";
-    case InferenceId::ARITH_NL_T_PURIFY_ARG: return "T_PURIFY_ARG";
-    case InferenceId::ARITH_NL_T_INIT_REFINE: return "T_INIT_REFINE";
-    case InferenceId::ARITH_NL_T_PI_BOUND: return "T_PI_BOUND";
-    case InferenceId::ARITH_NL_T_MONOTONICITY: return "T_MONOTONICITY";
-    case InferenceId::ARITH_NL_T_SECANT: return "T_SECANT";
-    case InferenceId::ARITH_NL_T_TANGENT: return "T_TANGENT";
-    case InferenceId::ARITH_NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE";
-    case InferenceId::ARITH_NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
-    case InferenceId::ARITH_NL_IAND_SUM_REFINE: return "IAND_SUM_REFINE";
-    case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "IAND_BITWISE_REFINE";
-    case InferenceId::ARITH_NL_CAD_CONFLICT: return "CAD_CONFLICT";
-    case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
-    case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT";
-    case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION";
+    case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
+    case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
+    case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
+      return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
+    case InferenceId::ARITH_NL_CM_QUADRATIC_EQ:
+      return "ARITH_NL_CM_QUADRATIC_EQ";
+    case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
+    case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
+    case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
+    case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS";
+    case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
+      return "ARITH_NL_INFER_BOUNDS_NT";
+    case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
+    case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
+      return "ARITH_NL_RES_INFER_BOUNDS";
+    case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
+    case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
+    case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
+    case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
+    case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
+    case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
+    case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
+    case InferenceId::ARITH_NL_IAND_INIT_REFINE:
+      return "ARITH_NL_IAND_INIT_REFINE";
+    case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
+      return "ARITH_NL_IAND_VALUE_REFINE";
+    case InferenceId::ARITH_NL_IAND_SUM_REFINE:
+      return "ARITH_NL_IAND_SUM_REFINE";
+    case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
+      return "ARITH_NL_IAND_BITWISE_REFINE";
+    case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
+    case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
+      return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
+    case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
+    case InferenceId::ARITH_NL_ICP_PROPAGATION:
+      return "ARITH_NL_ICP_PROPAGATION";
 
     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 6dacee33c..2891d5132 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -41,12 +41,16 @@ namespace theory {
 enum class InferenceId
 {
   // ---------------------------------- arith theory
-  //-------------------- core
+  //-------------------- preprocessing
+  ARITH_PP_ELIM_OPERATORS,
+  //-------------------- nonlinear core
   // simple congruence x=y => f(x)=f(y)
   ARITH_NL_CONGRUENCE,
   // shared term value split (for naive theory combination)
   ARITH_NL_SHARED_TERM_VALUE_SPLIT,
-  //-------------------- incremental linearization solver
+  // checkModel found a conflict with a quadratic equality
+  ARITH_NL_CM_QUADRATIC_EQ,
+  //-------------------- nonlinear incremental linearization solver
   // splitting on zero (NlSolver::checkSplitZero)
   ARITH_NL_SPLIT_ZERO,
   // based on sign (NlSolver::checkMonomialSign)
@@ -63,7 +67,7 @@ enum class InferenceId
   ARITH_NL_RES_INFER_BOUNDS,
   // tangent planes (NlSolver::checkTangentPlanes)
   ARITH_NL_TANGENT_PLANE,
-  //-------------------- transcendental solver
+  //-------------------- nonlinear transcendental solver
   // purification of arguments to transcendental functions
   ARITH_NL_T_PURIFY_ARG,
   // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
@@ -76,7 +80,7 @@ enum class InferenceId
   ARITH_NL_T_TANGENT,
   // secant refinement, the dual of the above inference
   ARITH_NL_T_SECANT,
-  //-------------------- iand solver
+  //-------------------- nonlinear iand solver
   // initial refinements (IAndSolver::checkInitialRefine)
   ARITH_NL_IAND_INIT_REFINE,
   // value refinements (IAndSolver::checkFullRefine)
@@ -85,12 +89,12 @@ enum class InferenceId
   ARITH_NL_IAND_SUM_REFINE,
   // bitwise refinements (IAndSolver::checkFullRefine)
   ARITH_NL_IAND_BITWISE_REFINE,
-  //-------------------- cad solver
+  //-------------------- nonlinear cad solver
   // conflict / infeasible subset obtained from cad
   ARITH_NL_CAD_CONFLICT,
   // excludes an interval for a single variable
   ARITH_NL_CAD_EXCLUDED_INTERVAL,
-  //-------------------- icp solver
+  //-------------------- nonlinear icp solver
   // conflict obtained from icp
   ARITH_NL_ICP_CONFLICT,
   // propagation / contraction of variable bounds from icp