diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp
index 5e82923f0..3838a88b5 100644
--- a/src/smt/smt_context_stat.cpp
+++ b/src/smt/smt_context_stat.cpp
@@ -32,7 +32,7 @@ namespace smt {
         return static_cast<unsigned>(acc / m_lemmas.size());
     }
 
-    void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
+    static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
         unsigned num_lits = cls->get_num_literals();
         for (unsigned i = 0; i < num_lits; i++) {
             literal l = cls->get_literal(i);
@@ -40,7 +40,7 @@ namespace smt {
         }
     }
 
-    void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
+    static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
         clause_vector::const_iterator it  = v.begin();
         clause_vector::const_iterator end = v.end();
         for (; it != end; ++it)
@@ -79,7 +79,7 @@ namespace smt {
         out << (m_assigned_literals.size() - n) << "]";
     }
 
-    void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
+    static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
         unsigned num_lits = cls->get_num_literals();
         for (unsigned i = 0; i < num_lits; i++) {
             literal l = cls->get_literal(i);
@@ -87,7 +87,7 @@ namespace smt {
         }
     }
 
-    void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
+    static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
         clause_vector::const_iterator it  = v.begin();
         clause_vector::const_iterator end = v.end();
         for (; it != end; ++it)
@@ -114,7 +114,7 @@ namespace smt {
         out << "\n";
     }
 
-    void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
+    static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
         unsigned num_lits = cls->get_num_literals();
         bool_var min_var  = cls->get_literal(0).var();
         for (unsigned i = 1; i < num_lits; i++) {
@@ -125,7 +125,7 @@ namespace smt {
         var2num_min_occs[min_var]++;
     }
 
-    void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
+    static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
         clause_vector::const_iterator it  = v.begin();
         clause_vector::const_iterator end = v.end();
         for (; it != end; ++it)
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 8028feae6..ad1e55ba6 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -335,7 +335,7 @@ namespace smt {
         }
     }
 
-    bool find_arg(app * n, expr * t, expr * & other) {
+    static bool find_arg(app * n, expr * t, expr * & other) {
         SASSERT(n->get_num_args() == 2);
         if (n->get_arg(0) == t) {
             other = n->get_arg(1);
@@ -348,7 +348,7 @@ namespace smt {
         return false;
     }
 
-    bool check_args(app * n, expr * t1, expr * t2) {
+    static bool check_args(app * n, expr * t1, expr * t2) {
         SASSERT(n->get_num_args() == 2);
         return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
     }
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index a7f415aad..5329cd80f 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -363,9 +363,6 @@ namespace smt {
         }
     }
 
-    struct scoped_set_relevancy {
-    };
-
     bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
         SASSERT(md != 0);
         m_root2value = &root2value;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 9f7656471..ee92c4f61 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -188,7 +188,7 @@ namespace smt {
         }
     }
 
-    void check_no_arithmetic(static_features const & st, char const * logic) {
+    static void check_no_arithmetic(static_features const & st, char const * logic) {
         if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) 
             throw default_exception("Benchmark constains arithmetic, but specified loging does not support it.");
     }
@@ -231,21 +231,21 @@ namespace smt {
             (st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9;
     }
 
-    bool is_in_diff_logic(static_features const & st) {
+    static bool is_in_diff_logic(static_features const & st) {
         return 
             st.m_num_arith_eqs == st.m_num_diff_eqs && 
             st.m_num_arith_terms == st.m_num_diff_terms && 
             st.m_num_arith_ineqs == st.m_num_diff_ineqs;
     }
 
-    bool is_diff_logic(static_features const & st) {
+    static bool is_diff_logic(static_features const & st) {
         return 
             is_in_diff_logic(st) && 
             (st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0)
             ;
     }
 
-    void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
+    static void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
         if (st.m_num_uninterpreted_functions != 0)
             throw default_exception("Benchmark contains uninterpreted function symbols, but specified logic does not support them.");
     }
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index b84ae68f0..1312b0dea 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -53,26 +53,26 @@ struct aig {
     aig() {}
 };
 
-inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
-inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
-inline bool is_var(aig * n) { return n->m_children[0].is_null(); }
-inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
-inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
-inline unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
-inline aig_lit left(aig * n) { return n->m_children[0]; }
-inline aig_lit right(aig * n) { return n->m_children[1]; }
-inline aig_lit left(aig_lit const & n) { return left(n.ptr()); }
-inline aig_lit right(aig_lit const & n) { return right(n.ptr()); }
+static bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; }
+static bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; }
+static bool is_var(aig * n) { return n->m_children[0].is_null(); }
+static bool is_var(aig_lit const & n) { return is_var(n.ptr()); }
+static unsigned id(aig_lit const & n) { return n.ptr()->m_id; }
+static unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; }
+static aig_lit left(aig * n) { return n->m_children[0]; }
+static aig_lit right(aig * n) { return n->m_children[1]; }
+static aig_lit left(aig_lit const & n) { return left(n.ptr()); }
+static aig_lit right(aig_lit const & n) { return right(n.ptr()); }
 
 inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; }
 
-void unmark(unsigned sz, aig_lit const * ns) {
+static void unmark(unsigned sz, aig_lit const * ns) {
     for (unsigned i = 0; i < sz; i++) {
         ns[i].ptr()->m_mark = false;
     }
 }
 
-void unmark(unsigned sz, aig * const * ns) {
+static void unmark(unsigned sz, aig * const * ns) {
     for (unsigned i = 0; i < sz; i++) {
         ns[i]->m_mark = false;
     }