From: Tim King <taking@cs.nyu.edu>
Date: Wed, 8 Nov 2017 04:18:30 +0000 (-0800)
Subject: Initializing QModelBuilder members. (#1334)
X-Git-Tag: cvc5-1.0.0~5495
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9444927c027e96f0fce22398611b97c274eff6b3;p=cvc5.git

Initializing QModelBuilder members. (#1334)
---

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 8fd659009..a72293ea1 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -34,11 +34,11 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-
-QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ){
-
-}
+QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
+    : TheoryEngineModelBuilder(qe->getTheoryEngine()),
+      d_qe(qe),
+      d_addedLemmas(0),
+      d_triedLemmas(0) {}
 
 bool QModelBuilder::optUseModel() {
   return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
@@ -163,11 +163,15 @@ bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
   }
 }
 
-
-QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ), d_basisNoMatch( c ) {
-
-}
+QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
+    : QModelBuilder(c, qe),
+      d_basisNoMatch(c),
+      d_didInstGen(false),
+      d_numQuantSat(0),
+      d_numQuantInstGen(0),
+      d_numQuantNoInstGen(0),
+      d_numQuantNoSelForm(0),
+      d_instGenMatches(0) {}
 
 /*
 Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {