diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index d40aa93e9..63971a7d9 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1089,12 +1089,11 @@ class env {
     }
 
     z3::sort mk_sort(char const* s) {
-        z3::symbol sym = symbol(s);
-        return mk_sort(sym);
+        return m_context.uninterpreted_sort(s);
     }
 
     z3::sort mk_sort(z3::symbol& s) {
-        return z3::sort(m_context, Z3_mk_uninterpreted_sort(m_context, s));
+        return m_context.uninterpreted_sort(s);
     }
     
 public: