From 5ecc32e731fa0fc1d59841d4c47457ad64a6d4e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Apr 2021 20:46:25 -0700 Subject: [PATCH] #5215 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/q_ematch.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 820d2a532..58ceab662 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -410,10 +410,8 @@ namespace q { mam::ground_subterms(pat, m_ground); for (expr* g : m_ground) { euf::enode* n = ctx.get_egraph().find(g); - if (!n->is_attached_to(m_qs.get_id())) { - euf::theory_var v = m_qs.mk_var(n); - ctx.get_egraph().add_th_var(n, v, m_qs.get_id()); - } + if (!n->is_attached_to(m_qs.get_id())) + m_qs.mk_var(n); } }