diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index bd9af1985ba..0f8f15306ea 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -58,7 +58,8 @@ void QuantDSplit::checkOwnership(Node q) bool doSplit = false; QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference(); Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; - for( size_t i=0, nvars = q[0].getNumChildren(); i bvs; for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 86ea5223e4f..2e5ee03705f 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -69,7 +69,8 @@ class QuantDSplit : public QuantifiersModule { /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const override { return "QuantDSplit"; } /** */ - static Node split(NodeManager * nm, const Node& q, size_t index); + static Node split(NodeManager* nm, const Node& q, size_t index); + private: /** list of relevant quantifiers asserted in the current context */ NodeIntMap d_quant_to_reduce;