diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp
index deeb2b99c..91f354eda 100644
--- a/src/smt/params/qi_params.cpp
+++ b/src/smt/params/qi_params.cpp
@@ -35,6 +35,7 @@ void qi_params::updt_params(params_ref const & _p) {
     m_qi_lazy_threshold = p.qi_lazy_threshold();
     m_qi_cost = p.qi_cost();
     m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
+    m_qi_quick_checker = static_cast<quick_checker_mode>(p.qi_quick_checker());
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index a85365de0..151a42d24 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -36,6 +36,7 @@ def_module_params(module_name='smt',
                           ('qi.lazy_threshold', DOUBLE, 20.0, 'threshold for lazy quantifier instantiation'),
                           ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
                           ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
+                          ('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),