From 0dc5bad6e4300113e1d3e7f393762cb24d72ad29 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 1 Apr 2020 12:58:34 -0700
Subject: [PATCH] fix in patching of monics

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

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 8d8403440..6d31bba99 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1405,7 +1405,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
     for (unsigned l = 0; l < m.size(); l++) {
         lpvar k = m.vars()[l];
         if (!in_power(m.vars(), l) &&
-            var_is_int(k) && 
+            !var_is_int(k) && 
             !var_is_used_in_a_correct_monic(k) &&
             try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
             SASSERT(mul_val(m) == var_val(m));