From a60295020b243f122bc36d317bd15c1926b1810e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Jun 2021 11:03:28 -0700 Subject: [PATCH] #5324 --- src/sat/smt/q_mam.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 4220eb7d4..76965cd63 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -2256,6 +2256,8 @@ namespace q { #endif // It doesn't make sense to process an irrelevant enode. TRACE("mam_execute_core", tout << "EXEC " << t->get_root_lbl()->get_name() << "\n";); + if (!ctx.is_relevant(n)) + return false; SASSERT(ctx.is_relevant(n)); m_pattern_instances.reset(); m_min_top_generation.reset();