diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 1f43bbe36..dd0171c6a 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -32,6 +32,7 @@ namespace opt {
         m_msolver = 0;
         m_s = s;
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
+        TRACE("opt", tout << "maxsmt\n";);
         if (m_soft_constraints.empty()) {
             TRACE("opt", tout << "no constraints\n";);
             m_msolver = 0;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 7b9ca0a8d..ceab047b7 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -145,6 +145,7 @@ namespace opt {
 
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
         lbool is_sat = s.check_sat_core(0,0);
+        TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
         if (is_sat != l_true) {
             m_model = 0;
             return is_sat;
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index e5370e82d..980ad7037 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -235,6 +235,7 @@ namespace opt {
 
     lbool optsmt::lex(unsigned obj_index) {
         IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
+        TRACE("opt", tout << "optsmt:lex\n";);
         solver::scoped_push _push(*m_s);
         SASSERT(obj_index < m_vars.size());
         return basic_lex(obj_index);