diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index b5486ad86..15176190e 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -390,6 +390,8 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
 
 // x != 0 or y = 0 => |xy| >= |y|
 void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
+    if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,        
+        return;     // or smaller than 1
     rational rmv = abs(val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -490,6 +492,15 @@ bool basics::is_separated_from_zero(const factorization& f) const {
     return true;
 }
 
+bool basics::factorization_has_real(const factorization& f) const {
+    for (const factor& fc: f) {
+        lpvar j = var(fc);
+        if (!c().var_is_int(j))
+            return true;
+    }
+    return false;
+}
+
 
 // here we use the fact xy = 0 -> x = 0 or y = 0
 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {        
diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h
index 4272b9a59..57cee8339 100644
--- a/src/math/lp/nla_basics_lemmas.h
+++ b/src/math/lp/nla_basics_lemmas.h
@@ -103,5 +103,6 @@ struct basics: common {
     // -> |fc[factor_index]| <= |rm|
     void generate_pl(const monic& rm, const factorization& fc, int factor_index);   
     bool is_separated_from_zero(const factorization&) const;
+    bool factorization_has_real(const factorization&) const;
 };
 }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index d86ea83aa..669f646e1 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -283,8 +283,8 @@ public:
     const rational& get_upper_bound(unsigned j) const;
     const rational& get_lower_bound(unsigned j) const;    
     
-    bool zero_is_an_inner_point_of_bounds(lpvar j) const;
-    
+    bool zero_is_an_inner_point_of_bounds(lpvar j) const;    
+    bool var_is_int(lpvar j) const { return m_lar_solver.column_is_int(j); }
     int rat_sign(const monic& m) const;
     inline int rat_sign(lpvar j) const { return nla::rat_sign(val(j)); }