diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 0728a0bd4b8..1c4f04ddd82 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -323,6 +323,7 @@ class set_get_option_cmd : public cmd {
     symbol      m_produce_assertions;
     symbol      m_regular_output_channel;
     symbol      m_diagnostic_output_channel;
+    symbol      m_random_seed;
     symbol      m_verbosity;
     symbol      m_global_decls;
     symbol      m_global_declarations;
@@ -337,7 +338,7 @@ class set_get_option_cmd : public cmd {
             s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions ||
             s == m_produce_models || s == m_produce_assignments ||
             s == m_regular_output_channel || s == m_diagnostic_output_channel ||
-            s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
+            s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations ||
             s == m_produce_assertions || s == m_reproducible_resource_limit;
     }
 
@@ -358,6 +359,7 @@ class set_get_option_cmd : public cmd {
         m_produce_assertions(":produce-assertions"),
         m_regular_output_channel(":regular-output-channel"),
         m_diagnostic_output_channel(":diagnostic-output-channel"),
+        m_random_seed(":random-seed"),
         m_verbosity(":verbosity"),
         m_global_decls(":global-decls"),
         m_global_declarations(":global-declarations"),
@@ -501,7 +503,10 @@ class set_option_cmd : public set_get_option_cmd {
     }
 
     void set_next_arg(cmd_context & ctx, rational const & val) override {
-        if (m_option == m_reproducible_resource_limit) {
+        if (m_option == m_random_seed) {
+            ctx.set_random_seed(to_unsigned(val));
+        }
+        else if (m_option == m_reproducible_resource_limit) {
             ctx.params().set_rlimit(to_unsigned(val));
         }
         else if (m_option == m_verbosity) {
@@ -589,6 +594,9 @@ class get_option_cmd : public set_get_option_cmd {
         else if (opt == m_global_decls || opt == m_global_declarations) {
             print_bool(ctx, ctx.global_decls());
         }
+        else if (opt == m_random_seed) {
+            print_unsigned(ctx, ctx.random_seed());
+        }
         else if (opt == m_verbosity) {
             print_unsigned(ctx, get_verbosity_level());
         }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b3df1e1e0fd..8e844a40609 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -466,6 +466,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_interactive_mode(false),
     m_global_decls(false),
     m_print_success(m_params.m_smtlib2_compliant),
+    m_random_seed(0),
     m_produce_unsat_cores(false),
     m_produce_unsat_assumptions(false),
     m_produce_assignments(false),
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 14025986731..fa9c2f296ce 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -185,6 +185,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     bool                         m_interactive_mode;
     bool                         m_global_decls;
     bool                         m_print_success;
+    unsigned                     m_random_seed;
     bool                         m_produce_unsat_cores;
     bool                         m_produce_unsat_assumptions;
     bool                         m_produce_assignments;
@@ -336,6 +337,8 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     void print_unsupported(symbol const & s, int line, int pos) { print_unsupported_msg(); print_unsupported_info(s, line, pos); }
     bool global_decls() const { return m_global_decls; }
     void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
+    unsigned random_seed() const { return m_random_seed; }
+    void set_random_seed(unsigned s) { m_random_seed = s; }
     bool produce_models() const;
     bool produce_proofs() const;
     bool produce_unsat_cores() const;