From 4b7bd3a88132c2c2a3e25b8d93f642020a5981b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Mar 2020 12:59:24 -0700 Subject: [PATCH] fix #3536 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4727b2fbf..905f15bcc 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1833,8 +1833,9 @@ public: if (m_idiv_terms.empty()) { return true; } - bool all_divs_valid = true; - for (expr* n : m_idiv_terms) { + bool all_divs_valid = true; + for (unsigned i = 0; i < m_idiv_terms.size(); ++i) { + expr* n = m_idiv_terms[i]; expr* p = nullptr, *q = nullptr; VERIFY(a.is_idiv(n, p, q)); theory_var v = mk_var(n);