diff options
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 57778b4c8..615ff987a 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -126,6 +126,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) { return; } + Trace("quant-dsplit") << "QuantDSplit::check" << std::endl; NodeManager* nm = NodeManager::currentNM(); FirstOrderModel* m = d_quantEngine->getModel(); std::vector<Node> lemmas; @@ -134,6 +135,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) ++it) { Node q = it->first; + Trace("quant-dsplit") << "- Split quantifier " << q << std::endl; if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q) && d_added_split.find(q) == d_added_split.end()) { @@ -196,5 +198,6 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl; d_quantEngine->addLemma(lem, false); } + Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } |