From 379a1927e62fb60cf0b7ba2833e3ac6fa6da15fe Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 11 Jan 2020 17:36:49 -0800
Subject: [PATCH] fix a bug in nexvar()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_common.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index a76ca57e3..d975f0b56 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -143,7 +143,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
         if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) {
             mf *= c().m_lar_solver.column_lower_bound(k).x;
         } else if (c().m_nla_settings.horner_subs_fixed() == 2 &&
-                   c().var_is_fixed_to_zero(j)) {
+                   c().var_is_fixed_to_zero(k)) {
             return cn.mk_scalar(rational(0));
         }
         else {