From bc2441c1c47d684ea4be15276e83db87cf62c0ec Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 17 Jan 2026 20:32:41 +0000 Subject: [PATCH] Fix compilation error in aig_exporter.cpp - use correct iterator API Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/muz/rel/aig_exporter.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/rel/aig_exporter.cpp b/src/muz/rel/aig_exporter.cpp index 9b9355cd5..9cac2ba93 100644 --- a/src/muz/rel/aig_exporter.cpp +++ b/src/muz/rel/aig_exporter.cpp @@ -23,8 +23,8 @@ namespace datalog { m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m) { std::set predicates; - for (auto& [pred, _] : m_rules.get_grouped_rules()) - predicates.insert(pred); + for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it) + predicates.insert(it->m_key); for (auto& [pred, _] : *facts) predicates.insert(pred); @@ -98,8 +98,8 @@ namespace datalog { expr_ref_vector exprs(m); substitution subst(m); - for (auto& [pred, rules] : m_rules.get_grouped_rules()) { - for (rule* r : *rules) { + for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it) { + for (rule* r : *it->get_value()) { unsigned numqs = r->get_positive_tail_size(); if (numqs > 1) { throw default_exception("non-linear clauses not supported");