diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 3e1c6f0cd..a87d4959d 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -26,6 +26,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
     m_refine_inj_axiom        = p.refine_inj_axioms();
+    m_ng_lift_ite             = static_cast<lift_ite_kind>(p.q_lift_ite());
 }
 
 void preprocessor_params::updt_params(params_ref const & p) {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 5c77c67c2..46f2cf175 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -33,6 +33,7 @@ def_module_params(module_name='smt',
                           ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'),
                           ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
                           ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'),
+                          ('q.lift_ite', UINT, 0, '0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers'),
                           ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
                           ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
                           ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 1d58c3f11..db027104e 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -640,7 +640,8 @@ namespace smt {
         // It destroys the existing patterns.
         // m_params.m_macro_finder            = true; 
         
-        m_params.m_ng_lift_ite             = LI_CONSERVATIVE;
+        if (m_params.m_ng_lift_ite == LI_NONE)
+            m_params.m_ng_lift_ite         = LI_CONSERVATIVE;
         TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
         m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
         setup_arrays();
@@ -664,7 +665,8 @@ namespace smt {
         m_params.m_qi_lazy_threshold       = 20;
         // 
         m_params.m_macro_finder            = true;
-        m_params.m_ng_lift_ite             = LI_CONSERVATIVE; 
+        if (m_params.m_ng_lift_ite == LI_NONE)
+            m_params.m_ng_lift_ite         = LI_CONSERVATIVE;
         m_params.m_pi_max_multi_patterns   = 10; //<< it was used for SMT-COMP
         m_params.m_array_lazy_ieq          = true;
         m_params.m_array_lazy_ieq_delay    = 4;