diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 6b4acf604..ab5ee9a98 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -50,6 +50,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
+    validate_string_solver(m_string_solver);
     if (_p.get_bool("arith.greatest_error_pivot", false))
         m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_GREATEST_ERROR;
     else if (_p.get_bool("arith.least_error_pivot", false))
@@ -173,3 +174,9 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_dump_goal_as_smt);
     DISPLAY_PARAM(m_auto_config);
 }
+
+void smt_params::validate_string_solver(symbol const& s) const {
+    if (s == "z3str3" || s == "seq" || s == "empty" || s == "auto" || s == "none")
+        return;
+    throw default_exception("Invalid string solver value. Legal values are z3str3, seq, empty, auto, none");
+}
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index b2f898d4c..5a13c69ac 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -320,6 +320,8 @@ struct smt_params : public preprocessor_params,
     void updt_params(context_params const & p);
 
     void display(std::ostream & out) const;
+
+    void validate_string_solver(symbol const& s) const;
 };