diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 4f5ad86f2..29b34b799 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -260,7 +260,6 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
         else { m_ctx->assert_expr(bg[i]); }
 
     unsigned soft_sz = soft.size();
-#pragma unused(soft_sz)
     lbool res = internal_check_assumptions(hard, soft);
     if (!m_use_push_bg) { m_ctx->pop(1); }
 
diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp
index 1e4dc522f..557858ca4 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.cpp
+++ b/src/muz/spacer/spacer_unsat_core_learner.cpp
@@ -25,9 +25,7 @@ Revision History:
 namespace spacer
 {
 
-#pragma mark - proof iterators
 
-# pragma mark - main methods
 unsat_core_learner::~unsat_core_learner()
 {
     std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<unsat_core_plugin>());
@@ -262,7 +260,6 @@ void unsat_core_learner::finalize()
     }
 }
 
-#pragma mark - API
 
 bool unsat_core_learner::is_a_marked(proof* p)
 {
@@ -290,7 +287,6 @@ void unsat_core_learner::set_closed(proof* p, bool value)
         m_unsat_core.push_back(lemma);
     }
 
-# pragma mark - checking for b_symbols
 
 class collect_pure_proc {
     func_decl_set& m_symbs;
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index d0d443528..58c700dae 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -32,7 +32,6 @@ Revision History:
 namespace spacer
 {
 
-#pragma mark - unsat_core_plugin_lemma
 
 void unsat_core_plugin_lemma::compute_partial_core(proof* step)
 {
@@ -105,7 +104,6 @@ void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const
 }
 
 
-#pragma mark - unsat_core_plugin_farkas_lemma
 void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step)
 {
     ast_manager &m = m_learner.m;
@@ -285,7 +283,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
     }
 }
 
-#pragma mark - unsat_core_plugin_farkas_optimized
     void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step)
     {
         SASSERT(m_learner.is_a_marked(step));
@@ -444,7 +441,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
         res = mk_not(m, negated_linear_combination); //TODO: rewrite the get-method to return nonnegated stuff?
                     }
 
-#pragma mark - unsat_core_plugin_farkas_bounded
 
     void unsat_core_plugin_farkas_lemma_bounded::finalize()
                     {
@@ -557,7 +553,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
 
                     app_ref sum(m);
                     sum = util.mk_int(0);
-                    for (int k=0; k < n; ++k)
+                    for (unsigned k=0; k < n; ++k)
                         {
                         sum = util.mk_add(sum, util.mk_mul(coeffs[i][k].get(), bounded_vectors[j][k].get()));
                         }
@@ -579,7 +575,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
         {
             ptr_vector<app> literals;
             vector<rational> coefficients;
-                    for (int j=0; j < matrix.num_cols(); ++j)
+                    for (unsigned j=0; j < matrix.num_cols(); ++j)
             {
                         expr_ref evaluation(m);
 
@@ -601,7 +597,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
         }
     }
 
-#pragma mark - unsat_core_plugin_min_cut
     unsat_core_plugin_min_cut::unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner), m(m){}
 
     void unsat_core_plugin_min_cut::compute_partial_core(proof* step)