diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 3cebce7f6..57ae66b03 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -100,7 +100,7 @@ def mk_build_dirs():
 def check_vc_cmd_prompt():
     try:
         DEVNULL = open(os.devnull, 'wb')
-        subprocess.call(['cl'], stdin=DEVNULL, stderr=DEVNULL)
+        subprocess.call(['cl'], stdout=DEVNULL, stderr=DEVNULL)
     except:
         raise MKException("You must execute the mk_win_dist.py script on a Visual Studio Command Prompt")
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e14d5139c..ae375fc99 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -37,6 +37,7 @@ Notes:
 #include"well_sorted.h"
 #include"model_evaluator.h"
 #include"for_each_expr.h"
+#include"scoped_timer.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -1304,9 +1305,11 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
         m_solver->set_progress_callback(this);
+        unsigned timeout     = m_params.m_timeout;
         scoped_watch sw(*this);
         cancel_eh<solver> eh(*m_solver);
         scoped_ctrl_c ctrlc(eh);
+        scoped_timer timer(timeout, &eh);
         lbool r;
         try {
             r = m_solver->check_sat(num_assumptions, assumptions);
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 22122cd83..ec2fbc93c 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
+    m_soft_timeout = p.soft_timeout();
     if (_p.get_bool("arith.greatest_error_pivot", false))
         m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
     else if (_p.get_bool("arith.least_error_pivot", false))
@@ -48,7 +49,6 @@ void smt_params::updt_params(params_ref const & p) {
 
 void smt_params::updt_params(context_params const & p) {
     m_auto_config    = p.m_auto_config;
-    m_soft_timeout   = p.m_timeout;
     m_model          = p.m_model;
     m_model_validate = p.m_model_validate;
 }
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 1b8058b44..43dd1b586 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -14,6 +14,7 @@ def_module_params(module_name='smt',
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
+                          ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),