diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 70741fa67..d2184bacf 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2572,6 +2572,9 @@ namespace smt {
             if (m_n1 == 0 || !m_context.is_relevant(m_n1))                                                                                                              \
                 goto backtrack;                                                                                                                                         \
             update_max_generation(m_n1, nullptr);                                                                                                                       \
+            for (unsigned i = 0; i < static_cast<const get_cgr *>(m_pc)->m_num_args; ++i) {                                                                             \
+                m_used_enodes.push_back(std::make_tuple(m_n1->get_arg(i), m_args[i]));                                                                                  \
+            }                                                                                                                                                           \
             m_registers[static_cast<const get_cgr *>(m_pc)->m_oreg] = m_n1;                                                                                             \
             m_pc = m_pc->m_next;                                                                                                                                        \
             goto main_loop;