Fixing some coverity warnings (#2357)

9 files changed, 35 insertions, 20 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 192a6b433..eb3f6232d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -627,7 +627,8 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
     // score is lexographic ( bound vars, shared vars )
     int score_max_1 = -1;
     int score_max_2 = -1;
-    int score_index = -1;
+    unsigned score_index = 0;
+    bool set_score_index = false;
     for( unsigned i=0; i<pats.size(); i++ ){
       Node p = pats[i];
       if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
@@ -641,13 +642,17 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto
             score_2++;
           }
         }
-        if( score_index==-1 || score_1>score_max_1 || ( score_1==score_max_1 && score_2>score_max_2 ) ){
+        if (!set_score_index || score_1 > score_max_1
+            || (score_1 == score_max_1 && score_2 > score_max_2))
+        {
           score_index = i;
+          set_score_index = true;
           score_max_1 = score_1;
           score_max_2 = score_2;
         }
       }
     }
+    Assert(set_score_index);
     //update the variable bounds
     Node mp = pats[score_index];
     for( unsigned i=0; i<var_contains[mp].size(); i++ ){
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 3615ef6f4..b50deea11 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -838,6 +838,7 @@ Node Trigger::getInversion( Node n, Node x ) {
     return x;
   }else if( n.getKind()==PLUS || n.getKind()==MULT ){
     int cindex = -1;
+    bool cindexSet = false;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
         if( n.getKind()==PLUS ){
@@ -859,12 +860,15 @@ Node Trigger::getInversion( Node n, Node x ) {
         }
         x = Rewriter::rewrite( x );
       }else{
-        Assert( cindex==-1 );
+        Assert(!cindexSet);
         cindex = i;
+        cindexSet = true;
       }
     }
-    Assert( cindex!=-1 );
-    return getInversion( n[cindex], x );
+    if (cindexSet)
+    {
+      return getInversion(n[cindex], x);
+    }
   }
   return Node::null();
 }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 84104e51c..33c0a836b 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -117,8 +117,6 @@ public:
   CegConjecture* d_parent;
   /** is the syntax restricted? */
   bool d_is_syntax_restricted;
-  /** does the syntax allow ITE expressions? */
-  bool d_has_ite;
   /** collect terms */
   void collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts );
   /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 9e3553a0b..20cd1fd03 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -97,7 +97,10 @@ class SygusInvarianceTest
 class EvalSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
-  EvalSygusInvarianceTest() : d_kind(kind::UNDEFINED_KIND) {}
+  EvalSygusInvarianceTest()
+      : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
+  {
+  }
 
   /** initialize this invariance test
    *
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index c36bdbcbf..d36566d63 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -1177,7 +1177,8 @@ Node SygusUnifIo::constructSol(
 
       // for ITE
       Node split_cond_enum;
-      int split_cond_res_index = -1;
+      unsigned split_cond_res_index = 0;
+      bool set_split_cond_res_index = false;
 
       for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
       {
@@ -1204,9 +1205,8 @@ Node SygusUnifIo::constructSol(
           if (strat == strat_ITE && sc > 0)
           {
             EnumCache& ecache_cond = d_ecache[split_cond_enum];
-            Assert(split_cond_res_index >= 0);
-            Assert(split_cond_res_index
-                   < (int)ecache_cond.d_enum_vals_res.size());
+            Assert(set_split_cond_res_index);
+            Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size());
             prev = x.d_vals;
             bool ret = x.updateContext(
                 this,
@@ -1361,10 +1361,10 @@ Node SygusUnifIo::constructSol(
               Assert(ecache_child.d_enum_val_to_index.find(rec_c)
                      != ecache_child.d_enum_val_to_index.end());
               split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
+              set_split_cond_res_index = true;
               split_cond_enum = ce;
-              Assert(split_cond_res_index >= 0);
               Assert(split_cond_res_index
-                     < (int)ecache_child.d_enum_vals_res.size());
+                     < ecache_child.d_enum_vals_res.size());
             }
           }
           else
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index f1aa08c65..967226e94 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -310,8 +310,6 @@ class SygusUnifIo : public SygusUnif
    * register a new value for an enumerator.
    */
   bool d_check_sol;
-  /** whether we have solved the overall conjecture */
-  bool d_solved;
   /** The number of values we have enumerated for all enumerators. */
   unsigned d_cond_count;
   /** The solution for the function of this class, if one has been found */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 072766b21..af6be2e97 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -193,7 +193,10 @@ class SygusUnifRl : public SygusUnif
   class DecisionTreeInfo
   {
    public:
-    DecisionTreeInfo() {}
+    DecisionTreeInfo()
+        : d_unif(nullptr), d_strategy(nullptr), d_strategy_index(0)
+    {
+    }
     ~DecisionTreeInfo() {}
     /** initializes this class */
     void initialize(Node cond_enum,
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index b94ae0654..41923f7a1 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -277,7 +277,7 @@ struct StrategyRestrictions
 class SygusUnifStrategy
 {
  public:
-  SygusUnifStrategy() {}
+  SygusUnifStrategy() : d_qe(nullptr) {}
   /** initialize
    *
    * This initializes this class with function-to-synthesize f. We also call
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c777a0976..ce0100686 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2625,7 +2625,8 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
   }
   if( !pinfer.empty() ){
     //now, determine which of the possible inferences we want to add
-    int use_index = -1;
+    unsigned use_index = 0;
+    bool set_use_index = false;
     Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl;
     unsigned min_id = 9;
     unsigned max_index = 0;
@@ -2634,10 +2635,13 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form
       Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : ";
       Trace("strings-solve")
           << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl;
-      if( use_index==-1 || pinfer[i].d_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_index ) ){
+      if (!set_use_index || pinfer[i].d_id < min_id
+          || (pinfer[i].d_id == min_id && pinfer[i].d_index > max_index))
+      {
         min_id = pinfer[i].d_id;
         max_index = pinfer[i].d_index;
         use_index = i;
+        set_use_index = true;
       }
     }
     //send the inference