diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 445f49244..022ea52f3 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2395,7 +2395,9 @@ namespace smt {
                 goto backtrack;
 
             // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
-            m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
+            if (m_ast_manager.has_trace_stream()) {
+                m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
+            }
 
             m_pc = m_pc->m_next;
             goto main_loop;