diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 036763407..bf4dae9ff 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -384,6 +384,8 @@ class theory_lra::imp {
         lp().settings().bound_propagation() = BP_NONE != propagation_mode();
         lp().settings().m_enable_hnf = lpar.enable_hnf();
         lp().set_track_pivoted_rows(lpar.bprop_on_pivoted_rows());
+        lp().settings().report_frequency = lpar.rep_freq();
+        lp().settings().print_statistics = lpar.print_stats();
 
         // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
         unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
diff --git a/src/util/lp/lp_dual_core_solver_def.h b/src/util/lp/lp_dual_core_solver_def.h
index 984f2e560..fba192f06 100644
--- a/src/util/lp/lp_dual_core_solver_def.h
+++ b/src/util/lp/lp_dual_core_solver_def.h
@@ -738,7 +738,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
     lp_assert(d_is_correct());
     lp_assert(problem_is_dual_feasible());
     lp_assert(this->basis_heading_is_correct());
-    this->set_total_iterations(0);
+    //this->set_total_iterations(0);
     this->iters_with_no_cost_growing() = 0;
     do {
         if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over("", *this->m_settings.get_message_ostream())){
diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h
index 588e67756..a96abffd6 100644
--- a/src/util/lp/lp_primal_core_solver_def.h
+++ b/src/util/lp/lp_primal_core_solver_def.h
@@ -643,7 +643,7 @@ template <typename T, typename X>    void lp_primal_core_solver<T, X>::backup_an
 
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::init_run() {
     this->m_basis_sort_counter = 0; // to initiate the sort of the basis
-    this->set_total_iterations(0);
+    //   this->set_total_iterations(0);
     this->iters_with_no_cost_growing() = 0;
     init_inf_set();
     if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
diff --git a/src/util/lp/lp_primal_core_solver_tableau_def.h b/src/util/lp/lp_primal_core_solver_tableau_def.h
index a2f8367b9..f2b6309f2 100644
--- a/src/util/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/util/lp/lp_primal_core_solver_tableau_def.h
@@ -327,7 +327,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
     CASSERT("A_off", this->A_mult_x_is_off() == false);
         lp_assert(basis_columns_are_set_correctly());
         this->m_basis_sort_counter = 0; // to initiate the sort of the basis
-        this->set_total_iterations(0);
+        //  this->set_total_iterations(0);
         this->iters_with_no_cost_growing() = 0;
 		lp_assert(this->inf_set_is_correct());
         if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)