diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp
index c2c5dbe0d..c9bf3c443 100644
--- a/src/muz/spacer/spacer_itp_solver.cpp
+++ b/src/muz/spacer/spacer_itp_solver.cpp
@@ -290,16 +290,16 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
             learner.register_plugin(plugin_farkas_lemma);
         }
         else if (m_iuc_arith == 2)
-            {
-                unsat_core_plugin_farkas_lemma_optimized* plugin_farkas_lemma_optimized = alloc(unsat_core_plugin_farkas_lemma_optimized, learner,m);
-                learner.register_plugin(plugin_farkas_lemma_optimized);
-            }
+        {
+            unsat_core_plugin_farkas_lemma_optimized* plugin_farkas_lemma_optimized = alloc(unsat_core_plugin_farkas_lemma_optimized, learner,m);
+            learner.register_plugin(plugin_farkas_lemma_optimized);
+        }
         else if(m_iuc_arith == 3)
-            {
-                unsat_core_plugin_farkas_lemma_bounded* plugin_farkas_lemma_bounded = alloc(unsat_core_plugin_farkas_lemma_bounded, learner,m);
-                learner.register_plugin(plugin_farkas_lemma_bounded);
-            }
-
+        {
+            unsat_core_plugin_farkas_lemma_bounded* plugin_farkas_lemma_bounded = alloc(unsat_core_plugin_farkas_lemma_bounded, learner,m);
+            learner.register_plugin(plugin_farkas_lemma_bounded);
+        }
+        
         if (m_iuc == 2)
         {
             unsat_core_plugin_min_cut* plugin_min_cut = alloc(unsat_core_plugin_min_cut, learner, m);
diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h
index d81a9764d..0b01f0032 100644
--- a/src/muz/spacer/spacer_itp_solver.h
+++ b/src/muz/spacer/spacer_itp_solver.h
@@ -61,7 +61,6 @@ private:
     unsigned m_iuc;
     unsigned m_iuc_arith;
     bool m_print_farkas_stats;
-    bool m_print_farkas_stats;
 
     bool is_proxy(expr *e, app_ref &def);
     void undo_proxies_in_core(ptr_vector<expr> &v);