diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 1d38c0685..0fcb5b702 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -196,7 +196,7 @@ namespace {
         }
 
         lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
-            TRACE(solver_na2as, tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
+            TRACE(solver_na2as, tout << "smt_solver::check_sat_core:\n"; for (unsigned i = 0; i < num_assumptions; ++i) tout << mk_pp(assumptions[i], m) << "\n";);
             return m_context.check(num_assumptions, assumptions);
         }
 
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index e3e49ef01..2f1d05a13 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -61,7 +61,7 @@ struct append_assumptions {
 
 lbool solver_na2as::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
     append_assumptions app(m_assumptions, num_assumptions, assumptions);
-    TRACE(solver_na2as, display(tout););
+    TRACE(solver_na2as, display(tout, m_assumptions.size(), m_assumptions.data()););
     return check_sat_core2(m_assumptions.size(), m_assumptions.data());
 }