From 948bf9540f92a32da1450360a0e33e10dabbd7d2 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 19 Oct 2016 12:07:33 +0100
Subject: [PATCH] Fix for previous commit.

---
 src/smt/theory_arith_nl.h | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index df9a71aaa..d47ecaa4e 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -590,7 +590,7 @@ namespace smt {
         bool propagated = false;
         context & ctx = get_context();
         for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
-            theory_var v = m_nl_monomials.size();
+            theory_var v = m_nl_monomials[i];
             expr * m     = var2expr(v);
             if (!ctx.is_relevant(m))
                 continue;
@@ -705,7 +705,7 @@ namespace smt {
         unsigned n        = 0;
         numeral range;
         for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
-            theory_var v = m_nl_monomials.size();
+            theory_var v = m_nl_monomials[i];
             if (is_real(v))
                 continue;
             bool computed_epsilon = false;
@@ -2337,7 +2337,7 @@ namespace smt {
         var_set             already_found;
         svector<theory_var> vars;
         for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
-            theory_var v = m_nl_monomials.size();
+            theory_var v = m_nl_monomials[i];
             mark_var(v, vars, already_found);
             expr * n     = var2expr(v);
             SASSERT(is_pure_monomial(n));