From 2a0537af695c99b5d4eef821021ca88e5f4eacdf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Apr 2020 08:17:57 -0700 Subject: [PATCH] fix #3954 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_full.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 0586e303f..fc15916b6 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -89,7 +89,8 @@ namespace smt { d_full->m_parent_maps.push_back(s); m_trail_stack.push(push_back_trail(d_full->m_parent_maps)); if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) { - for (enode * n : d->m_parent_selects) { + for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) { + enode * n = d->m_parent_selects[i]; if (!m_params.m_array_cg || n->is_cgr()) { instantiate_select_map_axiom(n, s); } @@ -172,7 +173,8 @@ namespace smt { m_trail_stack.push(push_back_trail(consts)); consts.push_back(cnst); instantiate_default_const_axiom(cnst); - for (enode * n : d->m_parent_selects) { + for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) { + enode * n = d->m_parent_selects[i]; SASSERT(is_select(n)); instantiate_select_const_axiom(n, cnst); }