diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 519302c19..f1c407dc7 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -40,6 +40,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
         m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
     else if (_p.get_bool("arith.least_error_pivot", false))
         m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
+    theory_array_params::updt_params(_p);
 }
 
 void smt_params::updt_params(params_ref const & p) {
@@ -47,6 +48,7 @@ void smt_params::updt_params(params_ref const & p) {
     qi_params::updt_params(p);
     theory_arith_params::updt_params(p);
     theory_bv_params::updt_params(p);
+    // theory_array_params::updt_params(p);
     updt_local_params(p);
 }
 
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 43dd1b586..33c9a11ec 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -40,4 +40,7 @@ def_module_params(module_name='smt',
                           ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
-                          ('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
+                          ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
+                          ('array.weak', BOOL, False, 'weak array theory'),
+                          ('array.extensional', BOOL, True, 'extensional array theory')
+                          ))
diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h
index c1ae8ce32..a022bcadf 100644
--- a/src/smt/params/theory_array_params.h
+++ b/src/smt/params/theory_array_params.h
@@ -51,6 +51,9 @@ struct theory_array_params : public array_simplifier_params {
         m_array_lazy_ieq_delay(10) {
     }
 
+
+    void updt_params(params_ref const & _p);
+
 #if 0
     void register_params(ini_params & p) {
         p.register_int_param("array_solver", 0, 3, reinterpret_cast<int&>(m_array_mode), "0 - no array, 1 - simple, 2 - model based, 3 - full");