mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

make use of uninterpreted_sort shorthand

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-27 09:34:47 -07:00
parent 562ed61a24
commit 4f02d380aa
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
examples/tptp/tptp5.cpp
View file

@ -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: