Fixed a bunch of clang warnings. (#5637)

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 657298491dc11c057cb741a90f599d1aa4486d5c..4c93e5727c4c73663237aef3380654b28cf78c98 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -171,7 +171,7 @@ bool DType::resolve(const std::map<std::string, TypeNode>& resolutions,
 
   d_involvesExt = false;
   d_involvesUt = false;
-  for (const std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  for (const std::shared_ptr<DTypeConstructor>& ctor : d_constructors)
   {
     if (ctor->involvesExternalType())
     {

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index c58bb78e4d9f916a5f37035768ee9d1f7f2e3841..665e68d285d8d67bcf0ba677f5583841c0566e0b 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -41,7 +41,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);
@@ -269,7 +269,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/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index fa31eb41c7382641552eb6823ab8d2226d983ddd..aae347caf9db9623c76116bb8a360268d2a7c54b 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -271,16 +271,16 @@ MinisatSatSolver::Statistics::~Statistics() {
   d_registry->unregisterStat(&d_statTotLiterals);
 }
 
-void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
-  d_statStarts.setData(d_minisat->starts);
-  d_statDecisions.setData(d_minisat->decisions);
-  d_statRndDecisions.setData(d_minisat->rnd_decisions);
-  d_statPropagations.setData(d_minisat->propagations);
-  d_statConflicts.setData(d_minisat->conflicts);
-  d_statClausesLiterals.setData(d_minisat->clauses_literals);
-  d_statLearntsLiterals.setData(d_minisat->learnts_literals);
-  d_statMaxLiterals.setData(d_minisat->max_literals);
-  d_statTotLiterals.setData(d_minisat->tot_literals);
+void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
+  d_statStarts.setData(minisat->starts);
+  d_statDecisions.setData(minisat->decisions);
+  d_statRndDecisions.setData(minisat->rnd_decisions);
+  d_statPropagations.setData(minisat->propagations);
+  d_statConflicts.setData(minisat->conflicts);
+  d_statClausesLiterals.setData(minisat->clauses_literals);
+  d_statLearntsLiterals.setData(minisat->learnts_literals);
+  d_statMaxLiterals.setData(minisat->max_literals);
+  d_statTotLiterals.setData(minisat->tot_literals);
 }
 
 } /* namespace CVC4::prop */

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 6bdc4ced018c423ac406b3120c5d59f060beeed9..ce9b4923c62efc2ea3e6f1b587d6447b22130d64 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -161,7 +161,7 @@ void PfManager::getAssertions(Assertions& as,
     assertions.push_back(*i);
   }
   NodeManager* nm = NodeManager::currentNM();
-  for (const std::pair<Node, smt::DefinedFunction>& dfn : df)
+  for (const std::pair<const Node, const smt::DefinedFunction>& dfn : df)
   {
     Node def = dfn.second.getFormula();
     const std::vector<Node>& formals = dfn.second.getFormals();

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index e3cbea152bd3af21fbd4fdbbf9d0bf303cbede00..8b6ca3021641dd766f2916982aee39d4b0946665 100644 (file)
--- 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/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 8f0441c28359ce4a290c37d7f43a7635dc114a0a..17eb518a2f137a9781fa2996fa498036dd05e8ff 100644 (file)
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -228,7 +228,7 @@ void IAndUtils::addDefaultValue(
   {
     counters[i] = 0;
   }
-  for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table)
+  for (const auto& 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 9434a049105a5d1532d9bcaa345bbe8d6b9033de..dff43e568a6f68a88b0abbed7e91632523ebf0e1 100644 (file)
--- 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 88706350ba4d4fbd88873b7a00239168967f10a5..2de5daeb655465ccdda1b4c71243b8ba74423990 100644 (file)
--- 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/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index ba60b6a0ee4504d4c533e829a537f025df6dd496..6dbb847a604f0122ea6e9d20c59f4bb151edb762 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -23,21 +23,6 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
-namespace {
-
-/**
- * Ensure a is in the main phase:
- *   -pi <= a <= pi
- */
-inline Node mkValidPhase(TNode a, TNode pi)
-{
-  return mkBounded(
-      NodeManager::currentNM()->mkNode(Kind::MULT, mkRationalNode(-1), pi),
-      a,
-      pi);
-}
-}  // namespace
-
 TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model)
     : d_im(im), d_model(model)
 {

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4d4ec89b4a730a3fb39938729b44578e4850cfd2..b13bd6926e0f5ef3a22005f66cedeeeab9e0f72f 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1758,7 +1758,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
   Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-void TheoryArrays::propagate(RowLemmaType lem)
+void TheoryArrays::propagateRowLemma(RowLemmaType lem)
 {
   Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
                      << options::arraysPropagate() << std::endl;
@@ -1845,7 +1845,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   // If propagating, check propagations
   int prop = options::arraysPropagate();
   if (prop > 0) {
-    propagate(lem);
+    propagateRowLemma(lem);
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
@@ -1975,7 +1975,7 @@ bool TheoryArrays::dischargeLemmas()
 
     int prop = options::arraysPropagate();
     if (prop > 0) {
-      propagate(l);
+      propagateRowLemma(l);
       if (d_state.isInConflict())
       {
         return true;

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 5236324bc9c5e48a7bf0a5a9e22b60bad26e3fa4..7e4f0e36cb236821b85d7aa912df717043188068 100644 (file)
--- 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 propagateRowLemma(RowLemmaType lem);
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();
 

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dbee65d8c5c188808ac986f85b7265ed77a16fa9..69500fea00fc03c2aca6719f04b0f7ab50e88f41 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -142,7 +142,7 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
   if (all.size() == 1) { return conjunctions[0]; }
 
   NodeBuilder<> conjunction(kind::AND);
-  for (const Node& n : all) { conjunction << n; }
+  for (TNode n : all) { conjunction << n; }
   return conjunction;
 }
 
@@ -161,7 +161,7 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
   if (all.size() == 1) { return nodes[0]; }
 
   NodeBuilder<> disjunction(kind::OR);
-  for (const Node& n : all) { disjunction << n; }
+  for (TNode n : all) { disjunction << n; }
   return disjunction;
 }
 /* Create node of kind XOR. */

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index fde28fd269514b8d82346c1fd32b8796f6297128..18b75e6313fb6f4462ae9831c3eddfea34484c92 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1196,7 +1196,7 @@ void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz,
         sca.d_search_terms[tn].find(d);
     if (itt != sca.d_search_terms[tn].end())
     {
-      for (const TNode& t : itt->second)
+      for (const Node& t : itt->second)
       {
         if (!options::sygusSymBreakLazy()
             || d_active_terms.find(t) != d_active_terms.end())
@@ -1469,7 +1469,7 @@ void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& le
           int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz);
           std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth );
           if( itt!=itc->second.d_search_terms[tn].end() ){
-            for (const TNode& t : itt->second)
+            for (const Node& t : itt->second)
             {
               if (!options::sygusSymBreakLazy()
                   || (d_active_terms.find(t) != d_active_terms.end()

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index eeaa678d42c7c0b5919c8a7884a033c7dd774b87..e1390207799a5f1a207c9eac88f39f578a6d66c0 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -905,7 +905,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
               d_conj_count++;
             }else{
               std::vector< Node > bvs;
-              for (const std::pair<TypeNode, unsigned>& lhs_pattern :
+              for (const std::pair<const TypeNode, unsigned>& lhs_pattern :
                    d_pattern_var_id[lhs])
               {
                 for (unsigned j = 0; j <= lhs_pattern.second; j++)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 20d80779387aea52b5d3c93d8f80899a183c20e6..1f45fd85f207ce3f43e40d4a5c80384f8c43eff6 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1114,7 +1114,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)
     {
@@ -1188,7 +1188,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 55beea4ca51ec004bbb07dcc063b29a0bbf93782..f0999a5daaec262c546e614c1b11a65e9dbc3be5 100644 (file)
--- 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 auto& etp : ev_to_pt)
       {
         if (etp.second.size() < d_deqThresh)
         {

diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 098af62a7db346886d0ed5e99dcd0d79a368f093..360476399fe2af239097dc37e74f1295f9341bbd 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -88,7 +88,7 @@ void EnumStreamPermutation::reset(Node value)
       d_var_classes[ti.getSubclassForVar(var)].push_back(var);
     }
   }
-  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
   {
     d_perm_state_class.push_back(PermutationState(p.second));
     if (Trace.isOn("synth-stream-concrete"))
@@ -383,7 +383,7 @@ void EnumStreamSubstitution::resetValue(Node value)
   d_curr_ind = 0;
   d_comb_state_class.clear();
   Trace("synth-stream-concrete") << " ..combining vars  :";
-  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
   {
     // ignore classes without variables being permuted
     unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 92754ebfe2889f06bb681a288f43875fcbea7d26..62eef124a7846d3f01cf84ce4d48e1fa27ab5e5a 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -126,7 +126,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds,
   {
     TypeNode svt = sv.getType();
     // is it equivalent to a previous variable?
-    for (const std::pair<Node, unsigned>& v : var_to_type_id)
+    for (const auto& v : var_to_type_id)
     {
       Node svc = v.first;
       if (svc.getType() == svt)

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 42677fa3fcde7226b08c1208f9f70c63df3fb007..f91cda36b7ed8c7e63a00d9191301fe14ed0892e 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -276,14 +276,14 @@ 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 (TNode ff : ops)
   {
-    for (const TNode& n : d_op_map[ff])
+    for (const Node& n : d_op_map[ff])
     {
       if (hasTermCurrent(n) && isTermActive(n))
       {
         computeArgReps(n);
-        TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n;
+        TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
         d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
       }
     }
@@ -312,7 +312,7 @@ void TermDb::computeUfTerms( TNode f ) {
   unsigned relevantCount = 0;
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
-  for (const Node& ff : ops)
+  for (TNode ff : ops)
   {
     std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
     if (it == d_op_map.end())

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index d03cc857039f3f99714237074dcb70a47aad7332..d9d9415fcd074c2c19a5cf106e347af85c01d9e5 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -755,7 +755,7 @@ 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/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index cb0540b8675e25f7b4e8ef88dadac6641662a988..5997d1217ea53895078e4a1cf0575442e3927c27 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -165,7 +165,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
       const std::map<Node, Node>& negativeMembers =
           d_state.getNegativeMembers(representative);
 
-      for (const std::pair<Node, Node>& negativeMember : negativeMembers)
+      for (const auto& negativeMember : negativeMembers)
       {
         Node member = nm->mkNode(MEMBER, negativeMember.first, univ);
         // negativeMember.second is the reason for the negative membership and

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e44c3c7a6aee815cad904c465a084049341e0496..4390b3e6e54bc8cb99e88f8dac953af7db5ea3dc 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1163,7 +1163,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
   {
     const std::map<TypeNode, std::vector<TNode> >& slackElements =
         d_cardSolver->getFiniteTypeSlackElements();
-    for (const std::pair<TypeNode, std::vector<TNode> >& pair : slackElements)
+    for (const auto& pair : slackElements)
     {
       const std::vector<Node>& members =
           d_cardSolver->getFiniteTypeMembers(pair.first);

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index edd00c954948a45983663a16cc2beb417b2ced6f..48116bc240a5d09e7f209559999d940c6765f41a 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -2575,7 +2575,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii)
     addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]);
   }
   // send phase requirements
-  for (const std::pair<const Node, bool> pp : cii.d_pendingPhase)
+  for (const std::pair<const Node, bool>& pp : cii.d_pendingPhase)
   {
     Node ppr = Rewriter::rewrite(pp.first);
     d_im.addPendingPhaseRequirement(ppr, pp.second);

diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 7724b5137e69c6834a73fc4c77fc41d29302fbe2..5beaa4a00047737212c12cd095d2eb292b329a76 100644 (file)
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -61,9 +61,9 @@ void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
   // notice this is not critical for soundness: not doing the below incrementing
   // will only lead to overapproximating when antecedants are required in
   // explanations
-  for (const std::pair<Node, std::map<bool, unsigned> >& pe : d_expDep)
+  for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
   {
-    for (const std::pair<bool, unsigned>& pep : pe.second)
+    for (const auto& pep : pe.second)
     {
       // See if this can be incremented: it can if this literal is not relevant
       // to the current index, and hence it is not relevant for both c1 and c2.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c8812b1608e79d436a653f1471c5463c65887cfa..7b38bd844bfbe7e31425c33b8db078903a833e37 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1823,7 +1823,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 (TNode e : exp)
       {
         Trace("te-proof-exp") << "  " << e << std::endl;
       }

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f04ebbb605b5eee1a824e997f2fe9f39f1bc6092..2173c6922d56ef7756c66d5e4da8ea4ebe75c497 100644 (file)
--- 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 (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 6377f78b60daf085acaa188b7b1a5d280d9aee03..f04bc5ec1f5dfa2bbd9e89bb821121f1252feb8e 100644 (file)
--- 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 (TNode a : tassumps)
   {
     if (a == lit)
     {

diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index c4d6c9c82dc8a91f7178d97ada7022cb087f5ecd..2e0a9adf5412d35f06f0cca9eb9930888f989ce2 100644 (file)
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -594,7 +594,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
   subs.push_back(p1);
   repls.push_back(p1);
   repls.push_back(p0);
-  for (const Node nn : d_phi)
+  for (const Node& nn : d_phi)
   {
     Node s =
         nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
@@ -629,7 +629,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
     subs.clear();
     repls.clear();
     bool first = true;
-    for (const Node& nn : p)
+    for (TNode nn : p)
     {
       subs.push_back(nn);
       if(!first) {