diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 369209e49..88e95e517 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -55,10 +55,8 @@ namespace smt { bool is_int = m_autil.is_int(n->get_owner()); m_is_int.push_back(is_int); m_f_targets.push_back(f_target()); - typename matrix::iterator it = m_matrix.begin(); - typename matrix::iterator end = m_matrix.end(); - for (; it != end; ++it) { - it->push_back(cell()); + for (auto& rows : m_matrix) { + rows.push_back(cell()); } m_matrix.push_back(row()); row & r = m_matrix.back(); @@ -367,10 +365,8 @@ namespace smt { m_is_int.shrink(old_num_vars); m_f_targets.shrink(old_num_vars); m_matrix.shrink(old_num_vars); - typename matrix::iterator it = m_matrix.begin(); - typename matrix::iterator end = m_matrix.end(); - for (; it != end; ++it) { - it->shrink(old_num_vars); + for (auto& cells : m_matrix) { + cells.shrink(old_num_vars); } } }