1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8ec25dffd..6e0a71641 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -56,14 +56,26 @@ void TheoryModel::reset(){
 }
 
 Node TheoryModel::getValue(TNode n) const {
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) "
+                          << std::endl;
+
   //apply substitutions
   Node nn = d_substitutions.apply(n);
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:"
+                          << nn << std::endl;
+
   //get value in model
   nn = getModelValue(nn);
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: "
+                          << nn << std::endl;
+
   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
+
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
+                          << nn << std::endl;
   return nn;
 }
 
@@ -228,6 +240,8 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
 
 /** add substitution */
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
+  Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t
+                         << ", invalidateCache = " << invalidateCache << ")\n";
   if( !d_substitutions.hasSubstitution( x ) ){
     d_substitutions.addSubstitution( x, t, invalidateCache );
   } else {