diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-21 18:31:55 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-21 18:31:55 +0000 |
commit | 130de2a67cb3c9d4e009d921e3a60a669aedfaff (patch) | |
tree | 0b3b21b9ba1f1f5a3558cd0fe046ef305389269d /src | |
parent | 83adf1da4487fb73f149ee9c013b4afcbfb92a99 (diff) |
Added debugging output to --check-models. I've found this output quite useful while debugging.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/model.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
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); } } |