diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index 7c159746f..a01f95c71 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -284,7 +284,8 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
         // -- old hypothesis reducer while the new one is broken
         if (m_old_hyp_reducer)
         {
-            // preprocess proof in order to get a proof which is better suited for unsat-core-extraction
+            // preprocess proof in order to get a proof which is
+            // better suited for unsat-core-extraction
             if (m_print_farkas_stats)
             {
                 iuc_proof iuc_before(m, res.get(), B);
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 39db6129c..87f998486 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -60,12 +60,16 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const&
     m_solvers[1] = pm.mk_fresh2();
     m_fparams[1] = &pm.fparams2();
 
-    m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), p.spacer_iuc(),
+    m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]),
+                          p.spacer_iuc(),
                           p.spacer_iuc_arith(),
+                          p.spacer_iuc_print_farkas_stats(),
                           p.spacer_iuc_old_hyp_reducer(),
                           p.spacer_iuc_split_farkas_literals());
-    m_contexts[1] = alloc(spacer::iuc_solver, *(m_solvers[1]), p.spacer_iuc(),
+    m_contexts[1] = alloc(spacer::iuc_solver, *(m_solvers[1]),
+                          p.spacer_iuc(),
                           p.spacer_iuc_arith(),
+                          p.spacer_iuc_print_farkas_stats(),
                           p.spacer_iuc_old_hyp_reducer(),
                           p.spacer_iuc_split_farkas_literals());