diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 46e66aaec..aec2ab59f 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -887,20 +887,20 @@ public:
         m_array_fid = null_family_id;
     }
     void execute(cmd_context & ctx) override {
-        psort_decl * array_sort = ctx.find_psort_decl(m_array_sort);
-        if (array_sort == nullptr)
+        auto array_sort = ctx.find_psort_decl(m_array_sort);
+        if (!array_sort)
             throw cmd_exception("Array sort is not available");
         ptr_vector<sort> & array_sort_args = m_domain;
         sort_ref_buffer domain(ctx.m());
         unsigned arity = m_f->get_arity();
         for (unsigned i = 0; i < arity; ++i) {
             array_sort_args.push_back(m_f->get_domain(i));
-            domain.push_back(array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data()));
+            domain.push_back((*array_sort)->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data()));
             array_sort_args.pop_back();
         }
         sort_ref range(ctx.m());
         array_sort_args.push_back(m_f->get_range());
-        range = array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data());
+        range = (*array_sort)->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data());
         parameter p(m_f);
         func_decl_ref new_map(ctx.m());
         new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, &p, domain.size(), domain.data(), range.get());
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b065607f6..42b19cfdc 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1166,10 +1166,11 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
     throw cmd_exception("invalid function declaration reference, unknown indexed function ", s);
 }
 
-psort_decl * cmd_context::find_psort_decl(symbol const & s) const {
+std::optional<psort_decl*> cmd_context::find_psort_decl(symbol const & s) const {
     psort_decl * p = nullptr;
-    m_psort_decls.find(s, p);
-    return p;
+    if (m_psort_decls.find(s, p))
+        return p;
+    return std::nullopt;
 }
 
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 8a742824b..eb4a84de4 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -20,6 +20,7 @@ Notes:
 --*/
 #pragma once
 
+#include<optional>
 #include<sstream>
 #include<vector>
 #include "util/stopwatch.h"
@@ -470,7 +471,7 @@ public:
     func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                unsigned arity, sort * const * domain, sort * range);
     recfun::promise_def decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range);
-    psort_decl * find_psort_decl(symbol const & s) const;
+    std::optional<psort_decl*> find_psort_decl(symbol const & s) const;
     cmd * find_cmd(symbol const & s) const;
     sexpr * find_user_tactic(symbol const & s) const;
     object_ref * find_object_ref(symbol const & s) const;
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 3f04ad9f0..8e7ec0dbe 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -582,12 +582,12 @@ namespace smt2 {
         sort * parse_sort_name(char const* context = "") {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
-            psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == nullptr)
+            auto d = m_ctx.find_psort_decl(id);
+            if (!d)
                 unknown_sort(id, context);
-            if (!d->has_var_params() && d->get_num_params() != 0)
+            if (!(*d)->has_var_params() && (*d)->get_num_params() != 0)
                 throw parser_exception("sort constructor expects parameters");
-            sort * r = d->instantiate(pm());
+            sort * r = (*d)->instantiate(pm());
             if (r == nullptr)
                 throw parser_exception("invalid sort application");
             next();
@@ -597,12 +597,12 @@ namespace smt2 {
         psort * parse_psort_name(bool ignore_unknown_sort = false) {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
-            psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d != nullptr) {
-                if (!d->has_var_params() && d->get_num_params() != 0)
+            auto d = m_ctx.find_psort_decl(id);
+            if (d) {
+                if (!(*d)->has_var_params() && (*d)->get_num_params() != 0)
                     throw parser_exception("sort constructor expects parameters");
                 next();
-                return pm().mk_psort_app(d);
+                return pm().mk_psort_app(*d);
             }
             else {
                 int idx = 0;
@@ -625,8 +625,8 @@ namespace smt2 {
             SASSERT(curr_id_is_underscore());
             next();
             symbol id = check_identifier_next("invalid indexed sort, symbol expected");
-            psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == nullptr)
+            auto d = m_ctx.find_psort_decl(id);
+            if (!d)
                 unknown_sort(id);
             sbuffer<unsigned> args;
             while (!curr_is_rparen()) {
@@ -635,7 +635,7 @@ namespace smt2 {
                 args.push_back(u);
                 next();
             }
-            sort * r = d->instantiate(pm(), args.size(), args.data());
+            sort * r = (*d)->instantiate(pm(), args.size(), args.data());
             if (r == nullptr)
                 throw parser_exception("invalid sort application");
             next();
@@ -645,13 +645,13 @@ namespace smt2 {
         void push_psort_app_frame() {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
-            psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == nullptr) {
+            auto d = m_ctx.find_psort_decl(id);
+            if (!d) {
                 unknown_sort(id);                                
             }
             next();
             void * mem      = m_stack.allocate(sizeof(psort_frame));
-            new (mem) psort_frame(*this, d, psort_stack().size());
+            new (mem) psort_frame(*this, *d, psort_stack().size());
         }
 
         void pop_psort_app_frame() {
@@ -708,12 +708,12 @@ namespace smt2 {
         void push_sort_app_frame() {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
-            psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == nullptr)
+            auto d = m_ctx.find_psort_decl(id);
+            if (!d)
                 unknown_sort(id);
             next();
             void * mem      = m_stack.allocate(sizeof(sort_frame));
-            new (mem) sort_frame(*this, d, sort_stack().size());
+            new (mem) sort_frame(*this, *d, sort_stack().size());
         }
 
         void pop_sort_app_frame() {
@@ -867,7 +867,7 @@ namespace smt2 {
 
             check_nonreserved_identifier("invalid sort declaration, symbol expected");
             symbol id = curr_id();
-            if (m_ctx.find_psort_decl(id) != nullptr)
+            if (m_ctx.find_psort_decl(id))
                 throw parser_exception("invalid sort declaration, sort already declared/defined");
             next();
             check_rparen("invalid sort declaration, ')' expected");
@@ -2273,7 +2273,7 @@ namespace smt2 {
 
             check_nonreserved_identifier("invalid sort declaration, symbol expected");
             symbol id = curr_id();
-            if (m_ctx.find_psort_decl(id) != nullptr)
+            if (m_ctx.find_psort_decl(id))
                 throw parser_exception("invalid sort declaration, sort already declared/defined");
             next();
             if (curr_is_rparen()) {
@@ -2298,7 +2298,7 @@ namespace smt2 {
             next();
             check_nonreserved_identifier("invalid sort definition, symbol expected");
             symbol id = curr_id();
-            if (m_ctx.find_psort_decl(id) != nullptr)
+            if (m_ctx.find_psort_decl(id))
                 throw parser_exception("invalid sort definition, sort already declared/defined");
             next();
             parse_sort_decl_params();