From a9d70fca1a0cdb073178521acea7200a9561f3ec Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 May 2022 19:09:10 -0700
Subject: [PATCH] fix #6061

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/arith_solver.cpp | 4 ++--
 src/smt/mam.cpp              | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 6d93b3378..66a4c2a65 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -321,7 +321,7 @@ namespace arith {
         reset_evidence();
         for (auto ev : e)
             set_evidence(ev.ci());
-        auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2);
+        auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2); // TODO add equality explanation
         ctx.propagate(n1, n2, jst->to_index());
         return true;
     }
@@ -756,7 +756,7 @@ namespace arith {
         set_evidence(ci4);
         enode* x = var2enode(v1);
         enode* y = var2enode(v2);
-        auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y);
+        auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y); // TODO add equality explanation
         ctx.propagate(x, y, jst->to_index());
     }
 
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a90403626..3d880aa80 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1952,7 +1952,7 @@ namespace {
                     m_args[i] = m_registers[pc->m_iregs[i]]->get_root();
                 SASSERT(n != 0);
                 do {
-                    if (n->get_decl() == f) {
+                    if (n->get_decl() == f && n->get_num_args() == num_args) {
                         unsigned i = 0;
                         for (; i < num_args; i++) {
                             if (n->get_arg(i)->get_root() != m_args[i])