diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 827405f85..8d3bc5995 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -66,8 +66,7 @@ namespace q { }; std::function _on_make = [&](euf::enode* n) { - relevant_eh(n); - + m_mam->add_node(n, false); }; ctx.get_egraph().set_on_merge(_on_merge); if (!ctx.relevancy().enabled())