From: Tim King <taking@cs.nyu.edu>
Date: Wed, 21 Nov 2012 18:31:55 +0000 (+0000)
Subject: Added debugging output to --check-models. I've found this output quite useful while... 
X-Git-Tag: cvc5-1.0.0~7571
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=130de2a67cb3c9d4e009d921e3a60a669aedfaff;p=cvc5.git

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

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);
       }
     }