diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 0d0c6d35a..42129be70 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -47,7 +47,6 @@ namespace opt {
         m_first(true),
         m_was_unknown(false) {
         m_params.updt_params(p);
-        std::cout << "Case split strategy " << m_params.m_case_split_strategy << "\n";
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
             m_params.m_relevancy_lvl = 0;
         }
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index f976e1d71..58505f8ac 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -26,6 +26,7 @@ namespace sat {
         m_always_true("always_true"),
         m_always_false("always_false"),
         m_caching("caching"),
+        m_restart_max(0),
         m_random("random"),
         m_geometric("geometric"),
         m_luby("luby"),
@@ -66,7 +67,8 @@ namespace sat {
 
         m_restart_initial = p.restart_initial();
         m_restart_factor  = p.restart_factor();
-        
+        m_restart_max     = p.restart_max();
+
         m_random_freq     = p.random_freq();
         m_random_seed     = p.random_seed();
         if (m_random_seed == 0) 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 0234b5710..1cdabddef 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -52,6 +52,7 @@ namespace sat {
         restart_strategy   m_restart;
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
+        unsigned           m_restart_max;
         double             m_random_freq;
         unsigned           m_random_seed;
         unsigned           m_burst_search;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 90e715a9d..80e6f403f 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -7,6 +7,7 @@ def_module_params('sat',
                           ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
                           ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
+                          ('restart.max', UINT, 0, 'maximal number of restarts. Ignored if set to 0'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
                           ('random_seed', UINT, 0, 'random seed'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e6fa15a4c..a5c9005df 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -744,7 +744,6 @@ namespace sat {
             simplify_problem();
             if (check_inconsistent()) return l_false;
 
-
             if (m_config.m_max_conflicts == 0) {
                 IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
                 return l_undef;
@@ -766,6 +765,12 @@ namespace sat {
                 simplify_problem();
                 if (check_inconsistent()) return l_false;
                 gc();
+
+                if (m_config.m_restart_max != 0 && m_config.m_restart_max <= m_restarts) {
+                    IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
+                    return l_undef;
+                }
+
             }
         }
         catch (abort_solver) {
@@ -1126,6 +1131,7 @@ namespace sat {
         m_restart_threshold       = m_config.m_restart_initial;
         m_luby_idx                = 1;
         m_gc_threshold            = m_config.m_gc_initial;
+        m_restarts                = 0;
         m_min_d_tk                = 1.0;
         m_stopwatch.reset();
         m_stopwatch.start();
@@ -1308,6 +1314,7 @@ namespace sat {
 
     void solver::restart() {
         m_stats.m_restart++;
+        m_restarts++;
         IF_VERBOSE(1,
                    verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
                    << " :restarts " << m_stats.m_restart << mk_stat(*this)
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index bcd9a66d2..aa45a1043 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -293,6 +293,7 @@ namespace sat {
 
     protected:
         unsigned m_conflicts;
+        unsigned m_restarts;
         unsigned m_conflicts_since_restart;
         unsigned m_restart_threshold;
         unsigned m_luby_idx;