From 130de2a67cb3c9d4e009d921e3a60a669aedfaff Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 21 Nov 2012 18:31:55 +0000
Subject: [PATCH] Added debugging output to --check-models. I've found this
 output quite useful while debugging.

---
 src/theory/model.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 33f482f8e..8dacf86e9 100644
--- 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);
       }
     }
-- 
2.30.2