diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index cf38719a9d8..7f1c1f268cc 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -2082,11 +2082,9 @@ namespace q {
                 p = p->get_root();
                 for (enode* p2 : euf::enode_parents(p)) {
                     if (p2->get_decl() == f &&
-                        num_args == n->num_args() && 
-                        num_args == p2->num_args() &&
                         ctx.is_relevant(p2) &&
                         p2->is_cgr() &&
-                        i < num_args && 
+                        i < p2->num_args() && 
                         p2->get_arg(i)->get_root() == p) {
                         v->push_back(p2);
                     }
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 0d09f07ead0..bc97daed2c5 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2109,11 +2109,9 @@ namespace {
                 for (; it2 != end2; ++it2) {
                     enode * p2 = *it2;
                     if (p2->get_decl() == f &&
-                        num_args == n->get_num_args() && 
-                        num_args == p2->get_num_args() &&
                         m_context.is_relevant(p2) &&
                         p2->is_cgr() &&
-                        i < num_args && 
+                        i < p2->get_num_args() && 
                         p2->get_arg(i)->get_root() == p) {
                         v->push_back(p2);
                     }