Address some coverity warnings, add another stat.

17 files changed, 46 insertions, 16 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index a0d9bda0f..8e8f34cac 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
   Assert( mpat.getKind()==INST_CONSTANT );
   d_f = quantifiers::TermDb::getInstConstAttr( mpat );
   d_index = mpat.getAttribute(InstVarNumAttribute());
+  d_firstTime = false;
 }
 
 void CandidateGeneratorQEAll::resetInstantiationRound() {
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 718d06c32..54415d974 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Assert( dt.isSygus() );
       //get the solution
       Node sol;
-      int status;
+      int status = -1;
       if( d_last_inst_si ){
         Assert( d_conj->getCegConjectureSingleInv() != NULL );
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 1f817da88..61a20ad42 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -329,9 +329,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
     if( is_cv ){  
       d_stack_vars.push_back( pv );
     }
-    if( vinst!=NULL ){
-      d_active_instantiators.erase( pv );
-    }
+    d_active_instantiators.erase( pv );
     unregisterInstantiationVariable( pv );
     return false;
   }
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f4eb67d74..11adc61fd 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -84,6 +84,9 @@ d_notify( *this ),
 d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
 d_ee_conjectures( c ){
   d_fullEffortCount = 0;
+  d_conj_count = 0;
+  d_subs_confirmCount = 0;
+  d_subs_unkCount = 0;
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
 
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index ceae3e4c8..2a940f1fd 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -741,17 +741,19 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
       Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
       //iterate over all classes except r
       tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
-        if( it->first!=r ){
-          InstMatch m( q );
-          m.add( baseMatch );
-          addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
-          if( qe->inConflict() ){
-            break;
+      if( tat ){
+        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+          if( it->first!=r ){
+            InstMatch m( q );
+            m.add( baseMatch );
+            addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+            if( qe->inConflict() ){
+              break;
+            }
           }
         }
+        tat = NULL;
       }
-      tat = NULL;
     }
   }
   Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 41c9c40c8..1f68fb787 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -597,6 +597,8 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term
 
 InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
 d_qe( qe ), d_notify(*this), d_qy( qe ){
+  d_icount = 1;
+  d_conflict = false;
 }
 
 bool InstPropagator::reset( Theory::Effort e ) {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index f432817fd..ac6e1edbe 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -625,6 +625,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
   : InstStrategyCbqi( qe ) {
   d_out = new CegqiOutputInstStrategy( this );
   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+  d_check_vts_lemma_lc = false;
 }
 
 InstStrategyCegqi::~InstStrategyCegqi() throw () {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index eab267747..c9f62243f 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -79,7 +79,7 @@ protected:
   //elimination information (for delayed elimination)
   class NestedQEInfo {
   public:
-    NestedQEInfo(){}
+    NestedQEInfo() : d_doVts(false){}
     ~NestedQEInfo(){}
     Node d_q;
     std::vector< Node > d_inst_terms;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 49e0a698f..c4bf61b28 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -155,6 +155,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe
     d_regenerate_frequency = 3;
     d_regenerate = true;
   }else{
+    d_regenerate_frequency = 1;
     d_regenerate = false;
   }
 }
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 582599680..976b81e60 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -33,6 +33,10 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
 
+QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){
+  d_ground_macros = false;
+}
+  
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
   unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 39ec2f0a1..60af7ad0a 100644
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -60,7 +60,7 @@ private:
   void addMacro( Node op, Node n, std::vector< Node >& opc );
   void debugMacroDefinition( Node oo, Node n );
 public:
-  QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){}
+  QuantifierMacros( QuantifiersEngine * qe );
   ~QuantifierMacros(){}
 
   bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9b25e27d4..1e484311c 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -967,7 +967,11 @@ MatchGen::MatchGen()
     d_n(),
     d_type( typ_invalid ),
     d_type_not()
-{}
+{
+  d_qni_size = 0;
+  d_child_counter = -1;
+  d_use_children = true;
+}
 
 
 MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
@@ -980,6 +984,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
     d_type(),
     d_type_not()
 {
+  //initialize temporary
+  d_child_counter = -1;
+  d_use_children = true;
+  
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 8bc8e1f04..aae8f6c5b 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -51,7 +51,10 @@ private:
   //what each literal does
   class RDomainLit {
   public:
-    RDomainLit() : d_merge(false){}
+    RDomainLit() : d_merge(false){
+      d_rd[0] = NULL;
+      d_rd[1] = NULL;
+    }
     ~RDomainLit(){}
     bool d_merge;
     RDomain * d_rd[2];
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 740e76d63..2c6bfb7d3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -91,6 +91,7 @@ TermDb::TermDb(context::Context* c, context::UserContext* u,
       d_op_id_count(0),
       d_typ_id_count(0),
       d_sygus_tdb(NULL) {
+  d_consistent_ee = true;
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 08faa8dc7..67990ef69 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1133,6 +1133,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     }
     if( d_term_db->isEntailed( q[1], subs, false, true ) ){
       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
+      ++(d_statistics.d_inst_duplicate_ent);
       return false;
     }
     //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
@@ -1520,6 +1521,7 @@ QuantifiersEngine::Statistics::Statistics()
       d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
       d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
       d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
+      d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
       d_triggers("QuantifiersEngine::Triggers", 0),
       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
@@ -1544,6 +1546,7 @@ QuantifiersEngine::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_instantiations);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
   smtStatisticsRegistry()->registerStat(&d_triggers);
   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
@@ -1570,6 +1573,7 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_instantiations);
   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
   smtStatisticsRegistry()->unregisterStat(&d_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d501cfc76..232d1d889 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -396,6 +396,7 @@ public:
     IntStat d_instantiations;
     IntStat d_inst_duplicate;
     IntStat d_inst_duplicate_eq;
+    IntStat d_inst_duplicate_ent;
     IntStat d_triggers;
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 92b18eed0..2ee367cfc 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -741,6 +741,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
         return ( s2 == r[0].getConst<String>() );
       } else {
         Assert( false, "RegExp contains variables" );
+        return false;
       }
     }
     case kind::REGEXP_CONCAT: {