diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 4ecec02c8..e6e879995 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -91,12 +91,12 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_probe(c, name);
         RESET_ERROR_CODE();
-        probe_info * p = mk_c(c)->find_probe(symbol(name));
-        if (p == nullptr) {
+        auto p = mk_c(c)->find_probe(symbol(name));
+        if (!p) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             RETURN_Z3(nullptr);
         }
-        probe * new_p = p->get();
+        probe * new_p = (*p)->get();
         RETURN_PROBE(new_p);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -404,12 +404,12 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_probe_get_descr(c, name);
         RESET_ERROR_CODE();
-        probe_info * p = mk_c(c)->find_probe(symbol(name));
-        if (p == nullptr) {
+        auto p = mk_c(c)->find_probe(symbol(name));
+        if (!p) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return "";
         }
-        return p->get_descr();
+        return (*p)->get_descr();
         Z3_CATCH_RETURN("");
     }
 
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 9f0b5d159..00abefeaa 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -767,9 +767,9 @@ MK_NARY_PROBE(mk_mul);
 
 probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
     if (n->is_symbol()) {
-        probe_info * pinfo = ctx.find_probe(n->get_symbol());
-        if (pinfo != nullptr)
-            return pinfo->get();
+        auto pinfo = ctx.find_probe(n->get_symbol());
+        if (pinfo)
+            return (*pinfo)->get();
         throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos());
     }
     else if (n->is_numeral()) {
diff --git a/src/cmd_context/tactic_manager.cpp b/src/cmd_context/tactic_manager.cpp
index d2dfe1c2c..f5dff041f 100644
--- a/src/cmd_context/tactic_manager.cpp
+++ b/src/cmd_context/tactic_manager.cpp
@@ -70,9 +70,10 @@ simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {
     return c;
 }
 
-probe_info * tactic_manager::find_probe(symbol const & s) const {
+std::optional<probe_info*> tactic_manager::find_probe(symbol const & s) const {
     probe_info * p = nullptr;
-    m_name2probe.find(s, p);
-    return p;
+    if (m_name2probe.find(s, p))
+        return p;
+    return std::nullopt;
 }
 
diff --git a/src/cmd_context/tactic_manager.h b/src/cmd_context/tactic_manager.h
index e9f9d9569..cc0afe7e0 100644
--- a/src/cmd_context/tactic_manager.h
+++ b/src/cmd_context/tactic_manager.h
@@ -38,7 +38,7 @@ public:
     void insert(simplifier_cmd* c);
     void insert(probe_info * p);
     std::optional<tactic_cmd*> find_tactic_cmd(symbol const & s) const; 
-    probe_info * find_probe(symbol const & s) const;     
+    std::optional<probe_info*> find_probe(symbol const & s) const;     
     simplifier_cmd* find_simplifier_cmd(symbol const& s) const;
 
     unsigned num_tactics() const { return m_tactics.size(); }