diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h
index 7da346dba..0f5b9ffcc 100644
--- a/src/ast/euf/euf_ac_plugin.h
+++ b/src/ast/euf/euf_ac_plugin.h
@@ -138,7 +138,7 @@ namespace euf {
         };
 
         theory_id                m_fid = 0;
-        unsigned                 m_op = null_decl_kind;
+        decl_kind                m_op = null_decl_kind;
         func_decl*               m_decl = nullptr;
         vector<eq>               m_eqs;
         ptr_vector<node>         m_nodes;
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 8462f2eea..519e724d9 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -20,6 +20,35 @@ Author:
 
 namespace sls {
 
+    template<typename num_t>
+    bool arith_base<num_t>::ineq::is_true() const {
+        switch (m_op) {
+        case ineq_kind::LE:
+            return m_args_value + m_coeff <= 0;
+        case ineq_kind::EQ:
+            return m_args_value + m_coeff == 0;
+        default:
+            return m_args_value + m_coeff < 0;
+        }
+    }
+
+    template<typename num_t>
+    std::ostream& arith_base<num_t>::ineq::display(std::ostream& out) const {
+        bool first = true;
+        for (auto const& [c, v] : m_args)
+            out << (first ? "" : " + ") << c << " * v" << v, first = false;
+        if (m_coeff != 0)
+            out << " + " << m_coeff;
+        switch (m_op) {
+        case ineq_kind::LE:
+            return out << " <= " << 0 << "(" << m_args_value + m_coeff << ")";
+        case ineq_kind::EQ:
+            return out << " == " << 0 << "(" << m_args_value + m_coeff << ")";
+        default:
+            return out << " < " << 0 << "(" << m_args_value + m_coeff << ")";
+        }
+    }    
+
     template<typename num_t>
     arith_base<num_t>::arith_base(context& ctx) :
         plugin(ctx),
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index 197cfda26..8dbbd37c9 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -57,31 +57,8 @@ namespace sls {
             num_t      m_args_value;
             unsigned   m_var_to_flip = UINT_MAX;
 
-            bool is_true() const {
-                switch (m_op) {
-                case ineq_kind::LE:
-                    return m_args_value + m_coeff <= 0;
-                case ineq_kind::EQ:
-                    return m_args_value + m_coeff == 0;
-                default:
-                    return m_args_value + m_coeff < 0;
-                }
-            }
-            std::ostream& display(std::ostream& out) const {
-                bool first = true;
-                for (auto const& [c, v] : m_args)
-                    out << (first ? "" : " + ") << c << " * v" << v, first = false;
-                if (m_coeff != 0)
-                    out << " + " << m_coeff;
-                switch (m_op) {
-                case ineq_kind::LE:
-                    return out << " <= " << 0 << "(" << m_args_value + m_coeff << ")";
-                case ineq_kind::EQ:
-                    return out << " == " << 0 << "(" << m_args_value + m_coeff << ")";
-                default:
-                    return out << " < " << 0 << "(" << m_args_value + m_coeff << ")";
-                }
-            }
+            bool is_true() const;
+            std::ostream& display(std::ostream& out) const;
         };
     private: