diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index bc994f0b3..f0e8fb59b 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -371,7 +371,7 @@ namespace smt {
             case l_true:
                 if (!m_proto_model->eval(n, res, false)) 
                     return true;
-                CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
+                CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 
                 if (m.is_false(res)) {
                     return false;
                 }
@@ -379,7 +379,7 @@ namespace smt {
             case l_false:
                 if (!m_proto_model->eval(n, res, false)) 
                     return true;
-                CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
+                CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 
                 if (m.is_true(res)) {
                     return false;
                 }