From 8e26c2af17f33439b20c90fc865152de67cfb2df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Dec 2023 13:05:21 -0800 Subject: [PATCH] fix #7049 Signed-off-by: Nikolaj Bjorner --- src/ast/polymorphism_inst.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp index 4da83ee10..aa9b1e5fe 100644 --- a/src/ast/polymorphism_inst.cpp +++ b/src/ast/polymorphism_inst.cpp @@ -94,7 +94,10 @@ namespace polymorphism { t.push(value_trail(m_decl_qhead)); for (; m_decl_qhead < num_decls; ++m_decl_qhead) { func_decl* p = m_decl_queue.get(m_decl_qhead); - for (expr* e : m_occurs[m.poly_root(p)]) + func_decl* r = m.poly_root(p); + if (!m_occurs.contains(r)) + continue; + for (expr* e : m_occurs[r]) instantiate(p, e, instances); } }