From 370706b2b7918c7c0a6580042c4306b58c6f43e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Aug 2017 14:33:37 -0700 Subject: [PATCH] patch Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index f59a57bf3..72a6d895c 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2086,6 +2086,7 @@ namespace smt { for (; it != end; ++it) { enode * p = *it; if (p->get_decl() == f && + p->get_num_args() > i && m_context.is_relevant(p) && p->is_cgr() && p->get_arg(i)->get_root() == n) {