diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index cc0f97ff0..fb81809b1 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -68,7 +68,10 @@ namespace sat {
         m_restart_factor  = p.restart_factor();
         
         m_random_freq     = p.random_freq();
-
+        m_random_seed     = p.random_seed();
+        if (m_random_seed == 0) 
+            m_random_seed = _p.get_uint("random_seed", 0);
+        
         m_burst_search    = p.burst_search();
         
         m_max_conflicts   = p.max_conflicts();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 90ebe968b..253786e11 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -53,6 +53,7 @@ namespace sat {
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
         double             m_random_freq;
+        unsigned           m_random_seed;
         unsigned           m_burst_search;
         unsigned           m_max_conflicts;
 
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 71579b86a..de0283897 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -9,6 +9,7 @@ def_module_params('sat',
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
                           ('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'),
                           ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
                           ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f4bf5393c..e7dee83ae 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -46,7 +46,7 @@ namespace sat {
         m_qhead(0),
         m_scope_lvl(0),
         m_params(p) {
-        m_config.updt_params(p);
+        updt_params(p);
     }
 
     solver::~solver() {
@@ -1972,7 +1972,7 @@ namespace sat {
         m_asymm_branch.updt_params(p);
         m_probing.updt_params(p);
         m_scc.updt_params(p);
-        m_rand.set_seed(p.get_uint("random_seed", 0));
+        m_rand.set_seed(m_config.m_random_seed);
     }
 
     void solver::collect_param_descrs(param_descrs & d) {