diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index e32c065aa..7d9e6e5be 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2241,6 +2241,9 @@ context::context(fixedpoint_params const&     params,
     m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts);
     m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts);
     m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts);
+
+    m_random.set_seed(m_params.spacer_random_seed());
+    m_children_order = static_cast<spacer_children_order>(m_params.spacer_order_children());
 }
 
 context::~context()
@@ -3680,7 +3683,12 @@ bool context::create_children(pob& n, datalog::rule const& r,
     unsigned_vector kid_order;
     kid_order.resize(preds.size(), 0);
     for (unsigned i = 0, sz = preds.size(); i < sz; ++i) kid_order[i] = i;
-    if (get_params().spacer_order_children() == 1) kid_order.reverse();
+    if (m_children_order == CO_REV_RULE) {
+        kid_order.reverse();
+    }
+    else if (m_children_order == CO_RANDOM) {
+        shuffle(kid_order.size(), kid_order.c_ptr(), m_random);
+    }
 
     for (unsigned i = 0, sz = preds.size(); i < sz; ++i) {
         unsigned j = kid_order[i];
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index e9881b3ff..ccdac2c48 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -782,6 +782,12 @@ public:
 
 };
 
+// order in which children are processed
+enum spacer_children_order {
+    CO_RULE,        // same order as in the rule
+    CO_REV_RULE,    // reverse order of the rule
+    CO_RANDOM       // random shuffle
+};
 
 class context {
 
@@ -819,6 +825,8 @@ class context {
     scoped_ptr<solver_pool> m_pool2;
 
 
+    random_gen           m_random;
+    spacer_children_order m_children_order;
     decl2rel             m_rels;         // Map from relation predicate to fp-operator.
     func_decl_ref        m_query_pred;
     pred_transformer*    m_query;