diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 411fdd1e1..4641a7b1b 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1801,7 +1801,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
     out.write(' {}\n')
     out.write('  static void collect_param_descrs(param_descrs & d) {\n')
     for param in params:
-        out.write('    d.insert("%s", %s, "%s", "%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param)))
+        out.write('    d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name))
     out.write('  }\n')
     if export:
         out.write('  /*\n')
diff --git a/src/util/params.cpp b/src/util/params.cpp
index a2609f840..cbb2b2acc 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -51,31 +51,34 @@ struct param_descrs::imp {
         param_kind   m_kind;
         char const * m_descr;
         char const * m_default;
+        char const * m_module;
 
-        info(param_kind k, char const * descr, char const * def):
+        info(param_kind k, char const * descr, char const * def, char const* module):
             m_kind(k),
             m_descr(descr),
-            m_default(def) {
+            m_default(def),
+            m_module(module) {
         }
 
         info():
             m_kind(CPK_INVALID), 
             m_descr(0), 
-            m_default(0) {
+            m_default(0),
+            m_module(0) {
         }
     };
 
     dictionary<info> m_info;
     svector<symbol> m_names;
 
-    void insert(symbol const & name, param_kind k, char const * descr, char const * def) {
+    void insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
         SASSERT(!name.is_numerical());
         info i;
         if (m_info.find(name, i)) {
             SASSERT(i.m_kind == k);
             return;
         }
-        m_info.insert(name, info(k, descr, def));
+        m_info.insert(name, info(k, descr, def, module));
         m_names.push_back(name);
     }
 
@@ -94,6 +97,13 @@ struct param_descrs::imp {
         return CPK_INVALID;
     }
 
+    char const* get_module(symbol const& name) const {
+        info i;
+        if (m_info.find(name, i)) 
+            return i.m_module;
+        return 0;
+    }
+
     char const * get_descr(symbol const & name) const {
         info i;
         if (m_info.find(name, i))
@@ -162,7 +172,7 @@ struct param_descrs::imp {
         dictionary<info>::iterator it  = other.m_imp->m_info.begin();
         dictionary<info>::iterator end = other.m_imp->m_info.end();
         for (; it != end; ++it) {
-            insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default);
+            insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module);
         }
     }
 
@@ -180,12 +190,12 @@ void param_descrs::copy(param_descrs & other) {
     m_imp->copy(other);
 }
 
-void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def) {
-    m_imp->insert(name, k, descr, def);
+void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
+    m_imp->insert(name, k, descr, def, module);
 }
 
-void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def) {
-    insert(symbol(name), k, descr, def);
+void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def, char const* module) {
+    insert(symbol(name), k, descr, def, module);
 }
 
 bool param_descrs::contains(char const * name) const {
@@ -236,6 +246,10 @@ symbol param_descrs::get_param_name(unsigned i) const {
     return m_imp->get_param_name(i);
 }
 
+char const* param_descrs::get_module(symbol const& name) const {
+    return m_imp->get_module(name);
+}
+
 void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
     return m_imp->display(out, indent, smt2_style, include_descr);
 }
@@ -297,11 +311,35 @@ public:
     void reset(symbol const & k);
     void reset(char const * k);
 
-    void validate(param_descrs const & p) const {
-        svector<params::entry>::const_iterator it  = m_entries.begin();  
-        svector<params::entry>::const_iterator end = m_entries.end();
+    bool split_name(symbol const& name, symbol & prefix, symbol & suffix) {
+        if (name.is_numerical()) return false;
+        char const* str = name.bare_str();
+        char const* period = strchr(str,'.');
+        if (!period) return false;
+        svector<char> prefix_((unsigned)(period-str), str);
+        prefix_.push_back(0);
+        prefix = symbol(prefix_.c_ptr());
+        suffix = symbol(period + 1);
+        return true;
+    }
+
+    void validate(param_descrs const & p) {
+        svector<params::entry>::iterator it  = m_entries.begin();  
+        svector<params::entry>::iterator end = m_entries.end();
+        symbol suffix, prefix;
         for (; it != end; ++it) {                                
             param_kind expected = p.get_kind(it->first);
+            if (expected == CPK_INVALID && split_name(it->first, prefix, suffix)) {                
+                expected = p.get_kind(suffix);
+                if (expected != CPK_INVALID) {
+                    if (symbol(p.get_module(suffix)) == prefix) {
+                        it->first = suffix;                    
+                    }
+                    else {
+                        expected = CPK_INVALID;
+                    }
+                }
+            }
             if (expected == CPK_INVALID) {
                 std::stringstream strm;
                 strm << "unknown parameter '" << it->first.str() << "'\n";    
@@ -490,7 +528,7 @@ void params_ref::display(std::ostream & out, symbol const & k) const {
         out << "default";
 }
 
-void params_ref::validate(param_descrs const & p) const {
+void params_ref::validate(param_descrs const & p) {
     if (m_params)
         m_params->validate(p);
 }
diff --git a/src/util/params.h b/src/util/params.h
index 06be486bb..f11374775 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -92,7 +92,7 @@ public:
     void display(std::ostream & out) const;
     void display_smt2(std::ostream& out, char const* module, param_descrs& module_desc) const;
 
-    void validate(param_descrs const & p) const;
+    void validate(param_descrs const & p);
 
     /*
       \brief Display the value of the given parameter.
@@ -115,8 +115,8 @@ public:
     param_descrs();
     ~param_descrs();
     void copy(param_descrs & other);
-    void insert(char const * name, param_kind k, char const * descr, char const * def = 0);
-    void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0);
+    void insert(char const * name, param_kind k, char const * descr, char const * def = 0, char const* module = 0);
+    void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0, char const* module = 0);
     bool contains(char const * name) const;
     bool contains(symbol const & name) const;
     void erase(char const * name);
@@ -130,6 +130,7 @@ public:
     void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const;
     unsigned size() const; 
     symbol get_param_name(unsigned idx) const;
+    char const * get_module(symbol const& name) const;
 };
 
 void insert_max_memory(param_descrs & r);