update

39 files changed, 48 insertions, 78 deletions

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 5c096767b..2bce4337e 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -40,7 +40,7 @@ const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks()
     const
 {
   std::map<Node, std::shared_ptr<ProofNode>> links;
-  for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+  for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
   {
     Assert(link.second);
     std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first);
@@ -268,7 +268,7 @@ void LazyCDProofChain::addLazyStep(Node expected,
     std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
     std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
     // add all current links in the chain
-    for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+    for (const std::pair<const Node, ProofGenerator* const>& link : d_gens)
     {
       allowedLeaves.push_back(link.first);
     }
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index a163e503d..9a689a380 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -182,9 +182,8 @@ void SymbolManager::Implementation::reset()
 
 // ---------------------------------------------- SymbolManager
 
-SymbolManager::SymbolManager(api::Solver* s)
-    : d_solver(s),
-      d_implementation(new SymbolManager::Implementation()),
+SymbolManager::SymbolManager()
+    : d_implementation(new SymbolManager::Implementation()),
       d_globalDeclarations(false)
 {
 }
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index a3ca8e780..a5dac1067 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -38,7 +38,7 @@ namespace CVC4 {
 class CVC4_PUBLIC SymbolManager
 {
  public:
-  SymbolManager(api::Solver* s);
+  SymbolManager();
   ~SymbolManager();
   /** Get the underlying symbol table */
   SymbolTable* getSymbolTable();
@@ -119,8 +119,6 @@ class CVC4_PUBLIC SymbolManager
   bool getGlobalDeclarations() const;
 
  private:
-  /** The API Solver object. */
-  api::Solver* d_solver;
   /**
    * The declaration scope that is "owned" by this symbol manager.
    */
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index b1a7c70b5..d99cd8df8 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,7 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
 
 CommandExecutor::CommandExecutor(Options& options)
     : d_solver(new api::Solver(&options)),
-      d_symman(new SymbolManager(d_solver.get())),
+      d_symman(new SymbolManager()),
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index fe37e9363..ceef3ae4a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -67,7 +67,7 @@ void throwLazyBBUnsupported(options::SatSolverMode m)
 
 }  // namespace
 
-OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
+OptionsHandler::OptionsHandler() {}
 
 unsigned long OptionsHandler::limitHandler(std::string option,
                                            std::string optarg)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 07e629976..847bc9e10 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -42,10 +42,11 @@ namespace options {
  */
 class OptionsHandler {
 public:
-  OptionsHandler(Options* options);
+ OptionsHandler();
 
-  void unsignedGreater0(const std::string& option, unsigned value) {
-    options::greater(0)(option, value);
+ void unsignedGreater0(const std::string& option, unsigned value)
+ {
+   options::greater(0)(option, value);
   }
 
   void unsignedLessEqual2(const std::string& option, unsigned value) {
@@ -114,9 +115,6 @@ public:
 
  private:
 
-  /** Pointer to the containing Options object.*/
-  Options* d_options;
-
   /* Help strings */
   static const std::string s_instFormatHelp;
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index af74fd31e..c1b814895 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -225,7 +225,7 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h
 
 Options::Options(OptionsListener* ol)
     : d_holder(new options::OptionsHolder()),
-      d_handler(new options::OptionsHandler(this)),
+      d_handler(new options::OptionsHandler()),
       d_olisten(ol)
 {}
 
diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp
index 441805758..555d72300 100644
--- a/src/prop/proof_post_processor.cpp
+++ b/src/prop/proof_post_processor.cpp
@@ -21,8 +21,8 @@ namespace CVC4 {
 namespace prop {
 
 ProofPostprocessCallback::ProofPostprocessCallback(
-    ProofNodeManager* pnm, ProofCnfStream* proofCnfStream)
-    : d_pnm(pnm), d_proofCnfStream(proofCnfStream)
+    ProofCnfStream* proofCnfStream)
+    : d_proofCnfStream(proofCnfStream)
 {
 }
 
@@ -88,7 +88,7 @@ bool ProofPostprocessCallback::update(Node res,
 
 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
                                      ProofCnfStream* proofCnfStream)
-    : d_cb(pnm, proofCnfStream), d_pnm(pnm)
+    : d_cb(proofCnfStream), d_pnm(pnm)
 {
 }
 
diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
index ced3e5b92..18ae8073e 100644
--- a/src/prop/proof_post_processor.h
+++ b/src/prop/proof_post_processor.h
@@ -36,8 +36,7 @@ namespace prop {
 class ProofPostprocessCallback : public ProofNodeUpdaterCallback
 {
  public:
-  ProofPostprocessCallback(ProofNodeManager* pnm,
-                           ProofCnfStream* proofCnfStream);
+  ProofPostprocessCallback(ProofCnfStream* proofCnfStream);
   ~ProofPostprocessCallback() {}
   /**
    * Initialize, called once for each new ProofNode to process. This initializes
@@ -72,8 +71,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
               bool& continueUpdate) override;
 
  private:
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
   /** The cnf stream proof generator */
   ProofCnfStream* d_proofCnfStream;
   //---------------------------------reset at the begining of each update
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index aa58ffa2c..00cd96b01 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -23,8 +23,7 @@ PropPfManager::PropPfManager(context::UserContext* userContext,
                              ProofNodeManager* pnm,
                              SatProofManager* satPM,
                              ProofCnfStream* cnfProof)
-    : d_pnm(pnm),
-      d_pfpp(new ProofPostproccess(pnm, cnfProof)),
+    : d_pfpp(new ProofPostproccess(pnm, cnfProof)),
       d_satPM(satPM),
       d_assertions(userContext)
 {
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index f3deee5bc..2696b2bda 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -73,8 +73,6 @@ class PropPfManager
   void checkProof(context::CDList<Node>* assertions);
 
  private:
-  /** A node manager */
-  ProofNodeManager* d_pnm;
   /** The proof post-processor */
   std::unique_ptr<prop::ProofPostproccess> d_pfpp;
   /**
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 98a2a7a36..bf7009081 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -31,8 +31,7 @@ Preprocessor::Preprocessor(SmtEngine& smt,
                            context::UserContext* u,
                            AbstractValues& abs,
                            SmtEngineStatistics& stats)
-    : d_context(u),
-      d_smt(smt),
+    : d_smt(smt),
       d_absValues(abs),
       d_propagator(true, true),
       d_assertionsProcessed(u, false),
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index cb83f969e..8700c3885 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -109,8 +109,6 @@ class Preprocessor
   void setProofGenerator(PreprocessProofGenerator* pppg);
 
  private:
-  /** A copy of the current context */
-  context::Context* d_context;
   /** Reference to the parent SmtEngine */
   SmtEngine& d_smt;
   /** Reference to the abstract values utility */
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index e3cbea152..8b6ca3021 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -39,7 +39,7 @@ namespace smt {
 class Assertions;
 class SmtEngineState;
 class Preprocessor;
-class SmtEngineStatistics;
+struct SmtEngineStatistics;
 
 /**
  * A solver for SMT queries.
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 831530995..d80272475 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -29,6 +29,7 @@ namespace theory {
 namespace arith {
 namespace nl {
 
+#ifdef CVC4_POLY_IMP
 CadSolver::CadSolver(InferenceManager& im, NlModel& model)
     : d_foundSatisfiability(false), d_im(im), d_model(model)
 {
@@ -38,6 +39,9 @@ CadSolver::CadSolver(InferenceManager& im, NlModel& model)
                                          "",
                                          NodeManager::SKOLEM_EXACT_NAME);
 }
+#else
+CadSolver::CadSolver(InferenceManager& im, NlModel& model) {}
+#endif
 
 CadSolver::~CadSolver() {}
 
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 4d537213f..344b0bb12 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -71,17 +71,17 @@ class CadSolver
   bool constructModelIfAvailable(std::vector<Node>& assertions);
 
  private:
+#ifdef CVC4_POLY_IMP
   /**
    * The variable used to encode real algebraic numbers to nodes.
    */
   Node d_ranVariable;
 
-#ifdef CVC4_POLY_IMP
   /**
    * The object implementing the actual decision procedure.
    */
   cad::CDCAC d_CAC;
-#endif
+
   /**
    * Indicates whether we found satisfiability in the last call to
    * checkFullRefine.
@@ -92,6 +92,7 @@ class CadSolver
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+#endif
 }; /* class CadSolver */
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp
index 050e6baed..e9a812e25 100644
--- a/src/theory/arith/nl/iand_table.cpp
+++ b/src/theory/arith/nl/iand_table.cpp
@@ -191,7 +191,8 @@ void IAndTable::addDefaultValue(
   {
     counters[i] = 0;
   }
-  for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table)
+  for (const std::pair<const std::pair<int64_t, int64_t>, uint64_t>& element :
+       table)
   {
     uint64_t result = element.second;
     counters[result]++;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 22a69cadb..9abe11afe 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -38,7 +38,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
     : d_containing(containing),
       d_im(containing.getInferenceManager()),
-      d_ee(ee),
       d_needsLastCall(false),
       d_checkCounter(0),
       d_extTheoryCb(ee),
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 21b978a55..ca97d6a9b 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -226,8 +226,6 @@ class NonlinearExtension
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
   InferenceManager& d_im;
-  // pointer to used equality engine
-  eq::EqualityEngine* d_ee;
   /** The statistics class */
   NlStats d_stats;
   // needs last call effort
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3e59aebe6..efc2eb3fe 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1752,7 +1752,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
   Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-void TheoryArrays::propagate(RowLemmaType lem)
+void TheoryArrays::propagateLemma(RowLemmaType lem)
 {
   Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
                      << options::arraysPropagate() << std::endl;
@@ -1839,7 +1839,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   // If propagating, check propagations
   int prop = options::arraysPropagate();
   if (prop > 0) {
-    propagate(lem);
+    propagateLemma(lem);
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
@@ -1969,7 +1969,7 @@ bool TheoryArrays::dischargeLemmas()
 
     int prop = options::arraysPropagate();
     if (prop > 0) {
-      propagate(l);
+      propagateLemma(l);
       if (d_state.isInConflict())
       {
         return true;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 5236324bc..87b629067 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -442,7 +442,7 @@ class TheoryArrays : public Theory {
   void checkStore(TNode a);
   void checkRowForIndex(TNode i, TNode a);
   void checkRowLemmas(TNode a, TNode b);
-  void propagate(RowLemmaType lem);
+  void propagateLemma(RowLemmaType lem);
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();
 
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 4d18ad926..4e5242c8a 100644
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -24,7 +24,7 @@ namespace bags {
 InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm), d_state(s)
+    : InferenceManagerBuffered(t, s, pnm)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 4b4edbaef..dc641e86f 100644
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -42,12 +42,6 @@ class InferenceManager : public InferenceManagerBuffered
   /** constants */
   Node d_true;
   Node d_false;
-  /**
-   * Reference to the state object for the theory of bags. We store the
-   * (derived) state here, since it has additional methods required in this
-   * class.
-   */
-  SolverState& d_state;
 };
 
 }  // namespace bags
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 60beef29f..e30444bd7 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -21,10 +21,8 @@ namespace CVC4 {
 namespace theory {
 namespace bags {
 
-TermRegistry::TermRegistry(SolverState& state, InferenceManager& im)
-    : d_im(im),
-      d_proxy(state.getUserContext()),
-      d_proxy_to_term(state.getUserContext())
+TermRegistry::TermRegistry(SolverState& state)
+    : d_proxy(state.getUserContext()), d_proxy_to_term(state.getUserContext())
 {
 }
 
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index d284126ee..79d575425 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -37,7 +37,7 @@ class TermRegistry
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
  public:
-  TermRegistry(SolverState& state, InferenceManager& im);
+  TermRegistry(SolverState& state);
 
   /**
    * Returns the existing empty bag for type tn
@@ -46,8 +46,6 @@ class TermRegistry
   Node getEmptyBag(TypeNode tn);
 
  private:
-  /** The inference manager */
-  InferenceManager& d_im;
   /** Map from bag terms to their proxy variables */
   NodeMap d_proxy;
   /** Backwards map of above */
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index bc4e0c8ae..7370d3816 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -426,7 +426,6 @@ ProofCircuitPropagatorForward::ProofCircuitPropagatorForward(
     ProofNodeManager* pnm, Node child, bool childAssignment, Node parent)
     : ProofCircuitPropagator{pnm},
       d_child(child),
-      d_childAssignment(childAssignment),
       d_parent(parent)
 {
 }
diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
index cc0aaad36..cebe3d751 100644
--- a/src/theory/booleans/proof_circuit_propagator.h
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -200,8 +200,6 @@ class ProofCircuitPropagatorForward : public ProofCircuitPropagator
  private:
   /** The current child that triggered the propagations */
   Node d_child;
-  /** The assignment of d_child */
-  bool d_childAssignment;
   /** The parent node used for propagation */
   Node d_parent;
 };
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6d7275fac..e62f1dbdf 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1200,7 +1200,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body,
   std::vector<Node> inactive_vars;
   std::map<Node, std::map<int, bool> > visited;
   std::map<Node, int> exclude;
-  for (const std::pair<Node, bool>& pr : qpr.d_phase_reqs)
+  for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
   {
     if (pr.first.getKind() == GEQ)
     {
@@ -1274,7 +1274,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body,
   } while (!evisit.empty() && !elig_vars.empty());
 
   bool ret = false;
-  for (const std::pair<Node, bool>& ev : elig_vars)
+  for (const std::pair<const Node, bool>& ev : elig_vars)
   {
     Node v = ev.first;
     Trace("var-elim-ineq-debug")
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 55beea4ca..79891cb42 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -83,7 +83,7 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
     }
     if (threshCount < 2)
     {
-      for (const std::pair<Node, std::vector<unsigned>>& etp : ev_to_pt)
+      for (const std::pair<const Node, std::vector<unsigned>>& etp : ev_to_pt)
       {
         if (etp.second.size() < d_deqThresh)
         {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 1a92cfc7f..d2fb68586 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -25,7 +25,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {}
+SygusQePreproc::SygusQePreproc() {}
 
 Node SygusQePreproc::preprocess(Node q)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 2214d4beb..2c49d9f58 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -40,17 +40,13 @@ namespace quantifiers {
 class SygusQePreproc
 {
  public:
-  SygusQePreproc(QuantifiersEngine* qe);
+  SygusQePreproc();
   ~SygusQePreproc() {}
   /**
    * Preprocess. Returns a lemma of the form q = nq where nq is obtained
    * by the quantifier elimination technique outlined above.
    */
   Node preprocess(Node q);
-
- private:
-  /** Pointer to quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 3e40d6654..cc82164b2 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -34,7 +34,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
     : QuantifiersModule(qe),
       d_tds(qe->getTermDatabaseSygus()),
       d_conj(nullptr),
-      d_sqp(qe)
+      d_sqp()
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(d_quantEngine, d_statistics)));
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 23448ca17..332230613 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -276,7 +276,7 @@ void TermDb::computeUfEqcTerms( TNode f ) {
     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
   }
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
-  for (const Node& ff : ops)
+  for (const TNode& ff : ops)
   {
     for (const Node& n : d_op_map[ff])
     {
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 4a7f4367e..383d3d16d 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -755,7 +755,8 @@ void TheorySep::postCheck(Effort level)
 
       // get model values
       std::map<int, Node> mvals;
-      for (const std::pair<int, Node>& sub_element : d_label_map[satom][slbl])
+      for (const std::pair<const int, Node>& sub_element :
+           d_label_map[satom][slbl])
       {
         int sub_index = sub_element.first;
         Node sub_lbl = sub_element.second;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e771f8bb8..450b319c9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1869,7 +1869,7 @@ theory::TrustNode TheoryEngine::getExplanation(
     if (Trace.isOn("te-proof-exp"))
     {
       Trace("te-proof-exp") << "Explanation is:" << std::endl;
-      for (const Node& e : exp)
+      for (const TNode& e : exp)
       {
         Trace("te-proof-exp") << "  " << e << std::endl;
       }
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index aaa3b44f7..903627794 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -26,7 +26,6 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
                                            MethodId ids)
     : d_ctx(c),
       d_subs(c),
-      d_pnm(pnm),
       d_tsubs(c),
       d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
       d_subsPg(
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index c316f08c5..26d152194 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -98,8 +98,6 @@ class TrustSubstitutionMap
   context::Context* d_ctx;
   /** The substitution map */
   SubstitutionMap d_subs;
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
   /** A context-dependent list of trust nodes */
   context::CDList<TrustNode> d_tsubs;
   /** Theory proof step buffer */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f04ebbb60..637cd05b7 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1286,7 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
     explainPredicate(atom, polarity, tassumptions);
   }
   // ensure that duplicates are removed
-  for (const TNode a : tassumptions)
+  for (const TNode& a : tassumptions)
   {
     if (std::find(assumptions.begin(), assumptions.end(), a)
         == assumptions.end())
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 6377f78b6..529179bbb 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -518,7 +518,7 @@ void ProofEqEngine::explainWithProof(Node lit,
   }
   Trace("pfee-proof") << "...got " << tassumps << std::endl;
   // avoid duplicates
-  for (const TNode a : tassumps)
+  for (const TNode& a : tassumps)
   {
     if (a == lit)
     {