From 4f02d380aa9d0fc95fd24975357fbff5825176b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2015 09:34:47 -0700 Subject: [PATCH] make use of uninterpreted_sort shorthand Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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: