Added debugging output to --check-models. I've found this output quite useful while...

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 33f482f8e11d181aec2150463465a888b261cc21..8dacf86e93597ddc161ffb46a576b12c2428c553 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -707,6 +707,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine);
       for ( ; !eqc_i.isFinished(); ++eqc_i) {
         Node n = *eqc_i;
+        static int repCheckInstance = 0;
+        ++repCheckInstance;
+
+        Debug("check-model::rep-checking")
+          << "( " << repCheckInstance <<") "
+          << "n: " << n << endl
+          << "getValue(n): " << tm->getValue(n) << endl
+          << "rep: " << rep << endl;
         Assert(tm->getValue(*eqc_i) == rep);
       }
     }