diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 1e0b07e9d..87974ea60 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -1229,6 +1229,9 @@ class using_params_tactical : public unary_tactical {
     params_ref m_params;
 public:
     using_params_tactical(tactic * t, params_ref const & p):unary_tactical(t), m_params(p) {
+        param_descrs r;
+        collect_param_descrs(r);
+        p.validate(r);
         t->updt_params(p);
     }
 
@@ -1276,7 +1279,7 @@ public:
                             model_converter_ref & mc, 
                             proof_converter_ref & pc, 
                             expr_dependency_ref & core) {
-        if (m_p->operator()(*(in.get())).is_true())
+        if (m_p->operator()(*(in.get())).is_true()) 
             m_t1->operator()(in, result, mc, pc, core);
         else
             m_t2->operator()(in, result, mc, pc, core);
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 4aff0de92..130b18cc9 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -302,10 +302,19 @@ public:
         svector<params::entry>::const_iterator end = m_entries.end();
         for (; it != end; ++it) {                                
             param_kind expected = p.get_kind(it->first);
-            if (expected == CPK_INVALID)
-                throw default_exception("unknown parameter '%s'", it->first.str().c_str());
-            if (it->second.m_kind != expected) 
-                throw default_exception("parameter kind mismatch '%s'", it->first.str().c_str());
+            if (expected == CPK_INVALID) {
+                std::stringstream strm;
+                strm << "unknown parameter '" << it->first.str() << "'\n";    
+                strm << "Legal parameters are:\n";
+                p.display(strm, 2, false, false);
+                throw default_exception(strm.str());
+            }
+            if (it->second.m_kind != expected) {
+                std::stringstream strm;
+                strm << "Parameter " << it->first.str() << " was given argument of type ";
+                strm << it->second.m_kind << ", expected " << expected;                
+                throw default_exception(strm.str());
+            }
         }
     }
     
@@ -347,11 +356,11 @@ public:
         out << "(params";
         svector<params::entry>::const_iterator it  = m_entries.begin();  
         svector<params::entry>::const_iterator end = m_entries.end();
-        for (; it != end; ++it) {                                
-            out << " " << it->first;
+        for (; it != end; ++it) {
+            out << " " << it->first;            
             switch (it->second.m_kind) {
             case CPK_BOOL:
-                out << " " << it->second.m_bool_value;
+                out << " " << (it->second.m_bool_value?"true":"false");
                 break;
             case CPK_UINT:
                 out << " " <<it->second.m_uint_value;
@@ -376,6 +385,41 @@ public:
         out << ")";
     }
 
+    void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
+        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        svector<params::entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {
+            if (!descrs.contains(it->first)) continue;
+            out << "(set-option :";
+            out << module << ".";        
+            out << it->first;
+            switch (it->second.m_kind) {
+            case CPK_BOOL:
+                out << " " << (it->second.m_bool_value?"true":"false");
+                break;
+            case CPK_UINT:
+                out << " " <<it->second.m_uint_value;
+                break;
+            case CPK_DOUBLE:
+                out << " " << it->second.m_double_value;
+                break;
+            case CPK_NUMERAL:
+                out << " " << *(it->second.m_rat_value);
+                break;
+            case CPK_SYMBOL:
+                out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
+                break;
+            case CPK_STRING:
+                out << " " << it->second.m_str_value;
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+            out << ")\n";
+        }
+    }
+
     void display(std::ostream & out, symbol const & k) const {
         svector<params::entry>::const_iterator it  = m_entries.begin();  
         svector<params::entry>::const_iterator end = m_entries.end();
@@ -423,10 +467,17 @@ params_ref::params_ref(params_ref const & p):
 void params_ref::display(std::ostream & out) const {
     if (m_params)
         m_params->display(out);
-    else
+    else 
         out << "(params)";
 }
 
+void params_ref::display_smt2(std::ostream& out, char const* module, param_descrs& descrs) const {
+    if (m_params)
+        m_params->display_smt2(out, module, descrs);
+
+}
+
+
 void params_ref::display(std::ostream & out, char const * k) const {
     display(out, symbol(k));
 }
diff --git a/src/util/params.h b/src/util/params.h
index 15be825b0..06be486bb 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -90,6 +90,7 @@ public:
     void set_sym(char const * k, symbol const & v);
 
     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;