diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index a8ab37473..8dcb16684 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -62,13 +62,13 @@ public:
         if (it == nullptr) return;
         mpq a = it->get_data().m_value;
         this->m_coeffs.erase(term_column);
-        for (const auto & p : t) {
+        for (auto p : t) {
             this->add_monomial(a * p.coeff(), p.column());
         }
     }
 
     lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
-        for (const auto & p : coeffs) {
+        for (auto const& p : coeffs) {
             add_monomial(p.first, p.second);
         }
     }
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index d31f09d06..2189b64e0 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -325,7 +325,7 @@ namespace {
         ast_manager &     m_manager;
         ptr_vector<expr>  m_queue;
         unsigned          m_head;
-        int               m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var          m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         ptr_vector<expr>  m_queue2;
         unsigned          m_head2;
         svector<scope>    m_scopes;
@@ -513,7 +513,7 @@ namespace {
         smt_params &m_params;  
         ptr_vector<expr>  m_queue;
         unsigned          m_head;
-        int               m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var          m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         bool_var_act_queue m_delayed_queue;
         svector<scope>    m_scopes;
     public:
@@ -745,7 +745,7 @@ namespace {
         ast_manager &        m_manager;
         ptr_vector<expr>     m_queue;
         unsigned             m_head;
-        int                  m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
+        bool_var             m_bs_num_bool_vars; //!< Number of boolean variable before starting to search.
         svector<queue_entry> m_queue2;
         svector<scope>       m_scopes;
         unsigned             m_current_generation;
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 49ec0cbe8..bc994f0b3 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -263,7 +263,7 @@ namespace smt {
     */
     bool context::check_th_diseq_propagation() const {
         TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
-        int num = get_num_bool_vars();
+        unsigned num = get_num_bool_vars();
         if (inconsistent() || get_manager().limit().is_canceled()) {
             return true;
         }
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index ed1dae13b..b93d10e8e 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -296,7 +296,7 @@ namespace smt {
 
     void context::display_hot_bool_vars(std::ostream & out) const {
         out << "hot bool vars:\n";
-        int num = get_num_bool_vars();
+        unsigned num = get_num_bool_vars();
         for (bool_var v = 0; v < num; v++) {
             double val = get_activity(v)/m_bvar_inc;
             if (val > 10.00) {
diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h
index edbca06c5..4b7fc4cc7 100644
--- a/src/smt/smt_types.h
+++ b/src/smt/smt_types.h
@@ -22,6 +22,7 @@ Revision History:
 #include "util/vector.h"
 #include "util/hashtable.h"
 #include "util/lbool.h"
+#include "util/sat_literal.h"
 
 class model;
 
@@ -29,9 +30,9 @@ namespace smt {
     /**
        \brief A boolean variable is just an integer.
     */
-    typedef int bool_var;
+    typedef sat::bool_var bool_var;
     
-    const bool_var null_bool_var  = -1;
+    const bool_var null_bool_var  = sat::null_bool_var;
     const bool_var true_bool_var  = 0;
     const bool_var first_bool_var = 1;