diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f17e40873..6e2fac4bd 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1018,7 +1018,7 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
 
 sort* basic_decl_plugin::join(sort* s1, sort* s2) {
     if (s1 == s2) return s1;
-    if (s1->get_family_id() == m_manager->m_arith_family_id && 
+    if (s1->get_family_id() == m_manager->m_arith_family_id &&
         s2->get_family_id() == m_manager->m_arith_family_id) {
         if (s1->get_decl_kind() == REAL_SORT) {
             return s1;
@@ -1030,6 +1030,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
     throw ast_exception(buffer.str().c_str());
 }
 
+
 func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
     switch (static_cast<basic_op_kind>(k)) {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index d4c9ecf79..f8948e3b6 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -210,6 +210,7 @@ namespace sat {
     public:
         bool inconsistent() const { return m_inconsistent; }
         unsigned num_vars() const { return m_level.size(); }
+        unsigned num_clauses() const;
         bool is_external(bool_var v) const { return m_external[v] != 0; }
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
@@ -446,8 +447,7 @@ namespace sat {
 
     protected:
         void display_binary(std::ostream & out) const;
-        void display_units(std::ostream & out) const;
-        unsigned num_clauses() const;
+        void display_units(std::ostream & out) const;        
         bool is_unit(clause const & c) const;
         bool is_empty(clause const & c) const;
         bool check_missed_propagation(clause_vector const & cs) const;
diff --git a/src/solver/solver.h b/src/solver/solver.h
index c4e1be13e..63592ea3b 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -139,6 +139,7 @@ public:
        \brief Display the content of this solver.
     */
     virtual void display(std::ostream & out) const;
+
     class scoped_push {
         solver& s;
         bool    m_nopop;
@@ -147,9 +148,9 @@ public:
         ~scoped_push() { if (!m_nopop) s.pop(1); }
         void disable_pop() { m_nopop = true; }
     };
+
 protected:
     virtual void set_cancel(bool f) = 0;
-
 };
 
 #endif