From 9e306e3b6ecc78b70e2bcc86db1b9bc75c515d6a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Sep 2021 20:50:35 -0700
Subject: [PATCH] more useful diagnostics

---
 src/smt/smt_context_inv.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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