diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index c3ae8c99b..04b974d6e 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -965,10 +965,19 @@ namespace smt {
     bool theory_arith<Ext>::propagate_linear_monomials() {
         TRACE("non_linear", tout << "propagating linear monomials...\n";);
         bool p = false;
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
-        for (; it != end; ++it) {
-            theory_var v = *it;
+        // CMW: m_nl_monomials is sometimes modified while executing
+        // propagate_linear_monomial(...), invalidating the iterator `it'.
+        // (Via the relevancy propagation that internalizes a new axiom
+        // in mk_div_axiom and possibly others.) I'm replacing the iterator
+        // with an index `i'.
+
+        // Was previously:
+        // svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
+        // svector<theory_var>::const_iterator end = m_nl_monomials.end();
+        // for (; it != end; ++it) {
+        //     theory_var v = *it;
+        for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
+            theory_var v = m_nl_monomials[i];
             if (propagate_linear_monomial(v))
                 p = true;
         }