diff --git a/lib/ni_solver.cpp b/lib/ni_solver.cpp
index be7272d36..a0341cb32 100644
--- a/lib/ni_solver.cpp
+++ b/lib/ni_solver.cpp
@@ -146,6 +146,12 @@ public:
         if (m_context)
             m_context->set_progress_callback(callback);
     }
+
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        smt::solver::collect_param_descrs(r);
+    }
+
 };
 
 solver * mk_non_incremental_smt_solver(cmd_context & ctx) {
diff --git a/lib/smt_solver.cpp b/lib/smt_solver.cpp
index 82b599869..6bdfd0524 100644
--- a/lib/smt_solver.cpp
+++ b/lib/smt_solver.cpp
@@ -181,10 +181,6 @@ namespace smt {
         void updt_params(params_ref const & p) {
             params2front_end_params(p, fparams());
         }
-
-        void collect_param_descrs(param_descrs & d) {
-            solver_front_end_params_descrs(d);
-        }
     };
 
     solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) {
@@ -346,8 +342,8 @@ namespace smt {
         return m_imp->updt_params(p);
     }
 
-    void solver::collect_param_descrs(param_descrs & d) const {
-        return m_imp->collect_param_descrs(d);
+    void solver::collect_param_descrs(param_descrs & d) {
+        solver_front_end_params_descrs(d);
     }
 
     context & solver::kernel() {
diff --git a/lib/smt_solver.h b/lib/smt_solver.h
index 68d85e8d6..1d04df9ed 100644
--- a/lib/smt_solver.h
+++ b/lib/smt_solver.h
@@ -228,7 +228,7 @@ namespace smt {
         /**
            \brief Collect a description of the configuration parameters.
         */
-        void collect_param_descrs(param_descrs & d) const;
+        static void collect_param_descrs(param_descrs & d);
 
         /**
            \brief Return a reference to the kernel.
diff --git a/lib/solver.cpp b/lib/solver.cpp
index 185223048..fd2be70d3 100644
--- a/lib/solver.cpp
+++ b/lib/solver.cpp
@@ -55,9 +55,16 @@ public:
     }
 
     virtual void collect_param_descrs(param_descrs & r) {
-        if (m_context == 0)
-            return;
-        m_context->collect_param_descrs(r);
+        if (m_context == 0) {
+            ast_manager m;
+            m.register_decl_plugins();
+            front_end_params p;
+            smt::solver s(m, p);
+            s.collect_param_descrs(r);
+        }
+        else {
+            m_context->collect_param_descrs(r);
+        }
     }
 
     virtual void init(ast_manager & m, symbol const & logic) {