diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 48c2df4a9..3875c0c9f 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -37,9 +37,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ", " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
         }
     }
 
@@ -64,9 +62,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ": " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
             return Z3_FALSE;
         }
     }
@@ -92,9 +88,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ": " << ex.msg();
-            warning_msg(buffer.str().c_str());
+            warning_msg(ex.msg());
         }
     }
 
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index d796dc9b1..d1184fbc8 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -86,7 +86,13 @@ void context_params::set(char const * param, char const * value) {
         set_bool(m_smtlib2_compliant, param, value);
     }
     else {
-        throw default_exception("unknown parameter '%s'", p.c_str());
+        param_descrs d;
+        collect_param_descrs(d);
+        std::stringstream strm;
+        strm << "unknown parameter '" << p << "'\n";
+        strm << "Legal parameters are:\n";
+        d.display(strm, 2, false, false);
+        throw default_exception(strm.str());
     }
 }
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 89ce99524..aeb70752b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3225,11 +3225,13 @@ namespace smt {
                 case QUASI_BASE:
                     SASSERT(m_columns[v].size() == 1);
                     del_row(get_var_row(v));
+                    TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
                     break; 
                 case BASE:
                     SASSERT(lazy_pivoting_lvl() != 0 || m_columns[v].size() == 1);
                     if (lazy_pivoting_lvl() > 0)
                         eliminate<false>(v, false);
+                    TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
                     del_row(get_var_row(v));
                     break;
                 case NON_BASE: {
@@ -3241,6 +3243,10 @@ namespace smt {
                         pivot<false>(r.get_base_var(), v, r[entry->m_row_idx].m_coeff, false);
                         SASSERT(is_base(v));
                         del_row(get_var_row(v));
+                        TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
+                    }
+                    else {
+                        TRACE("arith_make_feasible", tout << "no row v" << v << "\n";);
                     }
                     break;
                 } }
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 1d9426390..04acf1ad9 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -201,7 +201,7 @@ public:
         }
     }
 
-    void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) {
+    void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) {
         if (mod_name == symbol::null) {
             char const * new_name = get_new_param_name(param_name);
             if (new_name) {
@@ -213,11 +213,20 @@ public:
                                 param_name.bare_str());
             }
             else {
-                throw exception("unknown parameter '%s'", param_name.bare_str());
+                std::stringstream strm;
+                strm << "unknown parameter '" << param_name << "'\n";    
+                strm << "Legal parameters are:\n";
+                d.display(strm, 2, false, false);
+                throw default_exception(strm.str());
             }
         }
         else {
-            throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
+            std::stringstream strm;
+            strm << "unknown parameter '" << param_name << "' ";
+            strm << "at module '" << mod_name << "'\n";
+            strm << "Legal parameters are:\n";
+            d.display(strm, 2, false, false);
+            throw default_exception(strm.str());
         }
     }
 
@@ -225,7 +234,7 @@ public:
         param_kind k = d.get_kind(param_name);
         params_ref & ps = get_params(mod_name);
         if (k == CPK_INVALID) {
-            throw_unknown_parameter(param_name, mod_name);
+            throw_unknown_parameter(param_name, d, mod_name);
         }
         else if (k == CPK_UINT) {
             long val = strtol(value, 0, 10);
@@ -312,7 +321,7 @@ public:
 
     std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) {
         if (!d.contains(p)) {
-            throw_unknown_parameter(p, m);
+            throw_unknown_parameter(p, d, m);
         }
         char const * r = d.get_default(p);
         if (r == 0) 
@@ -478,7 +487,7 @@ public:
                         throw exception("unknown module '%s'", m.bare_str());
                 }
                 if (!d->contains(p))
-                    throw_unknown_parameter(p, m);
+                    throw_unknown_parameter(p, *d, m);
                 out << "  name:           " << p << "\n";
                 if (m != symbol::null) {
                     out << "  module:         " << m << "\n";