From 5509b468e95626e195732cc0dcda4d89402a550b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 31 Aug 2023 17:35:41 -0700
Subject: [PATCH] handle monomial_bounds::unit_propagate()

---
 src/math/lp/monomial_bounds.cpp | 16 +++++++++-------
 src/math/lp/nla_core.cpp        |  4 +---
 src/smt/theory_lra.cpp          |  3 ++-
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 84af29d05..28d287477 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -283,7 +283,7 @@ namespace nla {
                     break;
                 }
             }
-            lemma |= ineq(m.var(), lp::lconstraint_kind::EQ, 0);
+            lemma |= ineq(m.var(), lp::lconstraint_kind::NE, 0);
         }
         else {
             for (auto v : m) 
@@ -291,12 +291,14 @@ namespace nla {
                     lemma.explain_fixed(v);
             
             lpvar w = non_fixed_var(m);
-            SASSERT(w != null_lpvar);
-            
-            lp::lar_term term;
-            term.add_monomial(-m.rat_sign(), m.var());
-            term.add_monomial(k, w);
-            lemma |= ineq(term, lp::lconstraint_kind::EQ, 0);
+            if (w != null_lpvar) {
+                lp::lar_term term;
+                term.add_var(m.var());
+                term.add_monomial(-k, w);
+                lemma |= ineq(term, lp::lconstraint_kind::NE, 0);
+            } else {
+                lemma |= ineq(m.var(), lp::lconstraint_kind::NE, k);
+            }
         }
         
     }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 3ab89e012..0e87f8a1d 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1812,9 +1812,7 @@ bool core::improve_bounds() {
 }
     
 void core::propagate(vector<lemma>& lemmas) {
-    // disable for now
-    return;
-   // propagate linear monomials
+   // propagate linear monomials, those that have all, or all but one, variables fixed
     lemmas.reset();
     m_lemma_vec = &lemmas;
  
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 41426e0d6..31882ea11 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2150,9 +2150,10 @@ public:
         case l_true:
             propagate_basic_bounds();
             propagate_bounds_with_lp_solver();
+            propagate_nla();
             break;
         case l_undef:
-            propagate_nla();
+            UNREACHABLE();
             break;
         }
         return true;