diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index a5c907208..702e0898d 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -157,6 +157,7 @@ void context_params::updt_params(params_ref const & p) { void context_params::collect_param_descrs(param_descrs & d) { insert_rlimit(d); insert_timeout(d); + insert_ctrl_c(d); d.insert("well_sorted_check", CPK_BOOL, "type checker", "false"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); diff --git a/src/util/scoped_ctrl_c.cpp b/src/util/scoped_ctrl_c.cpp index 3b2c2bc45..55ff642df 100644 --- a/src/util/scoped_ctrl_c.cpp +++ b/src/util/scoped_ctrl_c.cpp @@ -19,6 +19,7 @@ Revision History: --*/ #include #include +#include "util/gparams.h" #include "util/scoped_ctrl_c.h" static std::mutex context_lock; @@ -73,6 +74,8 @@ scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled): m_first(true), m_once(once), m_enabled(enabled) { + if (gparams::get_value("ctrl_c") == "false") + m_enabled = false; if (m_enabled) { signal_lock(); active_contexts.push_back(this);