Address more coverity warnings (#2394)

diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index 4aef1231ccbcc20604facc2c0eb269322327dd78..a35ab2a035b0151d4fc78e480c26895ca77953bc 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -116,7 +116,6 @@ class ReqTrie
       std::vector<TypeNode> argts;
       if (tdb->canConstructKind(tn, d_req_kind, argts))
       {
-        bool ret = true;
         for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
              it != d_children.end();
              ++it)
@@ -134,10 +133,6 @@ class ReqTrie
             return false;
           }
         }
-        if (!ret)
-        {
-          return false;
-        }
       }
       else
       {

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 3df3717c3f96d96018dd0855b86024289b7350cd..e5df8db8a423dd0cc65430efe4937f350a4f2d35 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -321,7 +321,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
 
 CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen(
     std::vector<Node>& vars, unsigned nsamples)
-    : d_vars(vars.begin(), vars.end()), d_nsamples(nsamples)
+    : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples)
 {
 }
 

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 2a17f1e361a78960bf61e8084992a6801c406274..b90d98ca62c0933cbe85bf2e5b0a6b881803eea7 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -517,11 +517,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     activateInstantiationVariable(pv, i);
 
     //get the instantiator object
-    Instantiator * vinst = NULL;
-    std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv );
-    if( itin!=d_instantiator.end() ){
-      vinst = itin->second;
-    }
+    Assert(d_instantiator.find(pv) != d_instantiator.end());
+    Instantiator* vinst = d_instantiator[pv];
     Assert( vinst!=NULL );
     d_active_instantiators[pv] = vinst;
     vinst->reset(this, sf, pv, d_effort);

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index a3a0b8795b4e603afd51a5ae1cd27d8f574169c4..7d4684200045dd2cf5782621a4ecff552475a529 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -78,6 +78,7 @@ class TermGenerator
       : d_id(0),
         d_status(0),
         d_status_num(0),
+        d_status_child_num(0),
         d_match_status(0),
         d_match_status_child_num(0),
         d_match_mode(0)

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 6ea6e50b35613b50feeda699ce2376ad5da606fc..3f404c17fa4084bcb94c1f7490f260db3dc3acad 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -34,7 +34,10 @@ bool CandidateGenerator::isLegalCandidate( Node n ){
 }
 
 CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
-    : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0)
+    : CandidateGenerator(qe),
+      d_term_iter(-1),
+      d_term_iter_limit(0),
+      d_mode(cand_term_none)
 {
   d_op = qe->getTermDatabase()->getMatchOperator( pat );
   Assert( !d_op.isNull() );

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 8d8bf7f507d2c86864f9494d72454b5fad3e1e28..e28489b1a42cbd1dce093be60a15400f14d2b485 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -408,7 +408,10 @@ void BoundedIntegers::checkOwnership(Node f)
         bool setBoundVar = false;
         if( it->second==BOUND_INT_RANGE ){
           //must have both
-          if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){
+          std::map<Node, Node>& blm0 = bound_lit_map[0];
+          std::map<Node, Node>& blm1 = bound_lit_map[1];
+          if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end())
+          {
             setBoundedVar( f, v, BOUND_INT_RANGE );
             setBoundVar = true;
             for( unsigned b=0; b<2; b++ ){

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 392e092b8a4827d9b1f48ef3c04307fb19f93de6..15dd35c26bf4f48f99c1b2616cbc8f04d001da4a 100644 (file)
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -799,7 +799,8 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e
   }
   if( pol ){
     if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
-      Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl;
+      Trace("qip-rlv-propagate")
+          << "Relevant propagation : " << a << " == " << b << std::endl;
       Assert( d_qy.getEngine()->hasTerm( a ) );
       Assert( d_qy.getEngine()->hasTerm( b ) );
       Trace("qip-prop-debug") << "...equality between known terms." << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index af6be2e9753e0489bbd6763e65381badee441473..c9bdf56912f30af4b7a4b8bfa3af70dceca0a8fd 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -267,6 +267,7 @@ class SygusUnifRl : public SygusUnif
     class PointSeparator : public LazyTrieEvaluator
     {
      public:
+      PointSeparator() : d_dt(nullptr) {}
       /** initializes this class */
       void initialize(DecisionTreeInfo* dt);
       /**