diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 7bd21a1b5..004ea6754 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m,
     m_use_push_bg(p.spacer_keep_proxy())
 {
 
+    m_random.set_seed(p.spacer_random_seed());
     m_solvers[0] = solver0;
     m_solvers[1] = solver1;
 
@@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
     hard.append(_hard.size(), _hard.c_ptr());
     flatten_and(hard);
 
+    shuffle(hard.size(), hard.c_ptr(), m_random);
+
     m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
 
     // can be disabled if use_push_bg == true
diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h
index 1db65dc3e..0eed969bd 100644
--- a/src/muz/spacer/spacer_prop_solver.h
+++ b/src/muz/spacer/spacer_prop_solver.h
@@ -61,6 +61,8 @@ private:
     bool                m_use_push_bg;
     unsigned            m_current_level;    // set when m_in_level
 
+    random_gen          m_random;
+
     void assert_level_atoms(unsigned level);
 
     void ensure_level(unsigned lvl);