diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index a817a5e2b..809cbe1f9 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -689,7 +689,7 @@ namespace euf {
         if (ra->interpreted() && rb->interpreted()) {
             explain_eq(justifications, a, ra);
             explain_eq(justifications, b, rb);
-            return UINT_MAX;
+            return sat::null_bool_var;
         }
         expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
         m_tmp_eq->m_args[0] = a;
diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index f6f4b67de..218ffb3e5 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -19,6 +19,7 @@ Author:
 #include "util/id_var_list.h"
 #include "util/lbool.h"
 #include "util/approx_set.h"
+#include "util/sat_literal.h"
 #include "ast/ast.h"
 #include "ast/euf/euf_justification.h"
 
@@ -50,7 +51,7 @@ namespace euf {
         bool          m_merge_enabled = true; 
         bool          m_is_equality = false;    // Does the expression represent an equality
         lbool         m_value = l_undef;        // Assignment by SAT solver for Boolean node
-        unsigned      m_bool_var = UINT_MAX;    // SAT solver variable associated with Boolean node
+        sat::bool_var m_bool_var = sat::null_bool_var;    // SAT solver variable associated with Boolean node
         unsigned      m_class_size = 1;         // Size of the equivalence class if the enode is the root.
         unsigned      m_table_id = UINT_MAX;       
         unsigned      m_generation = 0;         // Tracks how many quantifier instantiation rounds were needed to generate this enode.
@@ -135,7 +136,7 @@ namespace euf {
         void set_merge_enabled(bool m) { m_merge_enabled = m; }
         void set_value(lbool v) { m_value = v; }
         void set_is_equality() { m_is_equality = true;  }
-        void set_bool_var(unsigned v) { m_bool_var = v; }
+        void set_bool_var(sat::bool_var v) { m_bool_var = v; }
 
     public:
         ~enode() { 
@@ -155,7 +156,7 @@ namespace euf {
         bool interpreted() const { return m_interpreted; }
         bool is_equality() const { return m_is_equality; }
         lbool value() const { return m_value;  }
-        unsigned bool_var() const { return m_bool_var; }
+        sat::bool_var bool_var() const { return m_bool_var; }
         bool is_cgr() const { return this == m_cg; }
         enode* get_cg() const { return m_cg; }
         bool commutative() const { return m_commutative; }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 17887535d..19164dff6 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -112,7 +112,7 @@ namespace arith {
             }
         };
         scoped_ptr_vector<internalize_state> m_internalize_states;
-        unsigned                      m_internalize_head{ 0 };
+        unsigned                      m_internalize_head = 0;
 
         class scoped_internalize_state {
             solver& m_imp;
@@ -149,10 +149,10 @@ namespace arith {
         vector<rational>         m_columns;
         var_coeffs               m_left_side;              // constraint left side
 
-        lpvar m_one_var   { UINT_MAX };
-        lpvar m_zero_var  { UINT_MAX };
-        lpvar m_rone_var  { UINT_MAX };
-        lpvar m_rzero_var { UINT_MAX };
+        lpvar m_one_var   = UINT_MAX;
+        lpvar m_zero_var  = UINT_MAX;
+        lpvar m_rone_var  = UINT_MAX;
+        lpvar m_rzero_var = UINT_MAX;
 
         enum constraint_source {
             inequality_source,
@@ -177,7 +177,7 @@ namespace arith {
         vector<lp_bounds>      m_bounds;
         unsigned_vector        m_unassigned_bounds;
         unsigned_vector        m_bounds_trail;
-        unsigned               m_asserted_qhead{ 0 };
+        unsigned               m_asserted_qhead = 0;
 
         svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates;
         unsigned                                          m_assume_eq_head{ 0 };
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 673885d85..1eb9d6aef 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -42,7 +42,7 @@ namespace euf {
         if (n) {
             if (m.is_bool(e)) {
                 SASSERT(!s().was_eliminated(n->bool_var()));
-                SASSERT(n->bool_var() != UINT_MAX);
+                SASSERT(n->bool_var() != sat::null_bool_var);
                 return literal(n->bool_var(), sign);
             }
             TRACE("euf", tout << "non-bool\n";);
@@ -153,7 +153,7 @@ namespace euf {
         enode* n = m_egraph.find(e);
         if (!n) 
             n = m_egraph.mk(e, m_generation, 0, nullptr); 
-        SASSERT(n->bool_var() == UINT_MAX || n->bool_var() == v);
+        SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
         m_egraph.set_bool_var(n, v);
         if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
             m_egraph.set_merge_enabled(n, false);