diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 556e84734..27fdd828b 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -173,7 +173,8 @@ public:
     }
 
     std::string get_value(char const * name) {
-        
+        // TODO
+        return "";
     }
 
 
@@ -200,9 +201,19 @@ void gparams::set(char const * name, char const * value) {
     g_imp->set(name, value);
 }
 
+void gparams::set(symbol const & name, char const * value) {
+    SASSERT(g_imp != 0);
+    g_imp->set(name.bare_str(), value);
+}
+
 std::string gparams::get_value(char const * name) {
     SASSERT(g_imp != 0);
-    g_imp->get_value(name);
+    return g_imp->get_value(name);
+}
+
+std::string gparams::get_value(symbol const & name) {
+    SASSERT(g_imp != 0);
+    return g_imp->get_value(name.bare_str());
 }
 
 void gparams::register_global(param_descrs & d) {
diff --git a/src/util/gparams.h b/src/util/gparams.h
index e02a8daa8..7112e67f9 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -24,8 +24,9 @@ Notes:
 class gparams {
     struct imp;
     static imp * g_imp; 
-    typedef z3_exception exception;
 public:
+    typedef default_exception exception;
+
     /**
        \brief Set a global parameter \c name with \c value.
        
@@ -44,6 +45,7 @@ public:
        An exception is thrown if the the parameter name is unknown, or if the value is incorrect.
     */
     static void set(char const * name, char const * value);
+    static void set(symbol const & name, char const * value);
     
     /**
        \brief Auxiliary method used to implement get-option in SMT 2.0 front-end.
@@ -53,6 +55,7 @@ public:
        An exception is thrown if the the parameter name is unknown.
     */
     static std::string get_value(char const * name);
+    static std::string get_value(symbol const & name);
     
     /**
        \brief Register additional global parameters
diff --git a/src/util/params.h b/src/util/params.h
index f587ed862..616f316bd 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -85,8 +85,8 @@ public:
       
       It displays 'default' if k is not in the parameter set.
     */
-    void display(std::ostream & out, char const * k);
-    void display(std::ostream & out, symbol const & k);
+    void display(std::ostream & out, char const * k) const;
+    void display(std::ostream & out, symbol const & k) const;
 };
 
 inline std::ostream & operator<<(std::ostream & out, params_ref const & ref) {