From 32c3a5af672ec03234054dbbc4a8f3c510996dce Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Aug 2024 17:56:34 -0700
Subject: [PATCH] include linear moves

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp | 10 +++++++++-
 src/ast/sls/sls_arith_base.h   |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index a70ed7ce4..b484520b9 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -1062,6 +1062,7 @@ namespace sls {
                 auto const& [w, c, monomial] = get_mul(v);
                 for (auto [w, p] : monomial) 
                     i.m_nonlinear.push_back({ w, { {v, coeff, p} } });
+                i.m_is_linear = false;
             }
             else
                 i.m_nonlinear.push_back({ v, { { v, coeff, 1 } } });
@@ -1755,7 +1756,14 @@ namespace sls {
                 find_quadratic_moves(*ineq, x, a, b, ineq->m_args_value);
             else
                 ;
-        }            
+        }        
+        if (!ineq->m_is_linear) {
+            for (auto const& [coeff, x] : ineq->m_args) {
+                if (is_fixed(x))
+                    continue;
+                find_linear_moves(*ineq, x, coeff, ineq->m_args_value);
+            }
+        }
     }
 
     template<typename num_t>
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index 90925b706..ae5881d20 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -63,6 +63,7 @@ namespace sls {
             vector<std::pair<var_t, vector<nonlinear_coeff>>> m_nonlinear;
             ineq_kind  m_op = ineq_kind::LE;            
             num_t      m_args_value;
+            bool       m_is_linear = true;
 
             bool is_true() const;
             std::ostream& display(std::ostream& out) const;