diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index a8f62572a..999ebab6b 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1056,7 +1056,6 @@ extern "C" {
             switch(_d->get_decl_kind()) {
             case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO;
             case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO;
-            case OP_SPECIAL_RELATION_PO_AO : return Z3_OP_SPECIAL_RELATION_PO_AO;
             case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
             case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
             default: UNREACHABLE();
diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp
index 40fde5083..e852c2b34 100644
--- a/src/api/api_special_relations.cpp
+++ b/src/api/api_special_relations.cpp
@@ -68,11 +68,21 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 #endif
+#define MK_TERN(NAME, FID)                                              \
+    Z3_ast Z3_API NAME(Z3_context c, unsigned index, Z3_ast a, Z3_ast b) { \
+    LOG_ ##NAME(c, index, a, b);                                        \
+    Z3_TRY;                                                             \
+    expr* args[2] = { to_expr(a), to_expr(b) };                         \
+    parameter p(index);                                                 \
+    ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_special_relations_fid(), FID, 1, &p, 2, args); \
+    mk_c(c)->save_ast_trail(a);                                         \
+    RETURN_Z3(of_ast(a));                                               \
+    Z3_CATCH_RETURN(nullptr);                                           \
+}
 
-    MK_BINARY(Z3_mk_sr_lo , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_LO, SKIP);
-    MK_BINARY(Z3_mk_sr_po , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO, SKIP);
-    MK_BINARY(Z3_mk_sr_po_ao,mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO_AO,SKIP);
-    MK_BINARY(Z3_mk_sr_plo, mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PLO, SKIP);
-    MK_BINARY(Z3_mk_sr_to , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_TO, SKIP);
+    MK_TERN(Z3_mk_linear_order, OP_SPECIAL_RELATION_LO);
+    MK_TERN(Z3_mk_partial_order, OP_SPECIAL_RELATION_PO);
+    MK_TERN(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO);
+    MK_TERN(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO);
 
 };
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index e18ca9204..8df43d477 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1707,42 +1707,27 @@ namespace z3 {
     */
     inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
 
-    inline expr sr_lo(expr const& a, expr const& b) {
+    typedef Z3_ast Z3_apply_order(Z3_context, unsigned, Z3_ast, Z3_ast);
+ 
+    inline expr apply_order(Z3_apply_order app, unsigned index, expr const& a, expr const& b) {
         check_context(a, b);
-        Z3_ast r = Z3_mk_sr_lo(a.ctx(), a, b);
+        Z3_ast r = app(a.ctx(), index, a, b);
         a.check_error();
         return expr(a.ctx(), r);
     }
-
-    inline expr sr_po(expr const& a, expr const& b) {
-        check_context(a, b);
-        Z3_ast r = Z3_mk_sr_po(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
+    inline expr linear_order(unsigned index, expr const& a, expr const& b) {
+        return apply_order(Z3_mk_linear_order, index, a, b);
     }
-
-    inline expr sr_po_ao(expr const& a, expr const& b) {
-        check_context(a, b);
-        Z3_ast r = Z3_mk_sr_po_ao(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
+    inline expr partial_order(unsigned index, expr const& a, expr const& b) {
+        return apply_order(Z3_mk_partial_order, index, a, b);
     }
-
-    inline expr sr_plo(expr const& a, expr const& b) {
-        check_context(a, b);
-        Z3_ast r = Z3_mk_sr_plo(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
+    inline expr piecewise_linear_order(unsigned index, expr const& a, expr const& b) {
+        return apply_order(Z3_mk_piecewise_linear_order, index, a, b);
     }
-
-    inline expr sr_to(expr const& a, expr const& b) {
-        check_context(a, b);
-        Z3_ast r = Z3_mk_sr_to(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
+    inline expr tree_order(unsigned index, expr const& a, expr const& b) {
+        return apply_order(Z3_mk_tree_order, index, a, b);
     }
 
-
     template<typename T> class cast_ast;
 
     template<> class cast_ast<ast> {
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 6d1db22b3..7ba33a61d 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3608,49 +3608,41 @@ extern "C" {
     /** @name Special relations */
     /*@{*/
     /**
-       \brief declare \c a and \c b are in linear order.
+       \brief declare \c a and \c b are in linear order over a relation indexed by \c id.
 
        \pre a and b are of same type.
+       
 
-       def_API('Z3_mk_sr_lo', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+       def_API('Z3_mk_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
      */
-    Z3_ast Z3_API Z3_mk_sr_lo(Z3_context c, Z3_ast a, Z3_ast b);
+    Z3_ast Z3_API Z3_mk_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
 
     /**
-       \brief declare \c a and \c b are in partial order.
+       \brief declare \c a and \c b are in partial order over a relation indexed by \c id.
 
        \pre a and b are of same type.
 
-       def_API('Z3_mk_sr_po', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+       def_API('Z3_mk_partial_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
      */
-    Z3_ast Z3_API Z3_mk_sr_po(Z3_context c, Z3_ast a, Z3_ast b);
+    Z3_ast Z3_API Z3_mk_partial_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
 
     /**
-       \brief declare \c a and \c b are already partial ordered.
+       \brief declare \c a and \c b are in piecewise linear order indexed by relation \c id.
 
        \pre a and b are of same type.
 
-       def_API('Z3_mk_sr_po_ao', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+       def_API('Z3_mk_piecewise_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
      */
-    Z3_ast Z3_API Z3_mk_sr_po_ao(Z3_context c, Z3_ast a, Z3_ast b);
+    Z3_ast Z3_API Z3_mk_piecewise_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
 
     /**
-       \brief declare \c a and \c b are in piecewise linear order.
+       \brief declare \c a and \c b are in tree order indexed by \c id.
 
        \pre a and b are of same type.
 
-       def_API('Z3_mk_sr_plo', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+       def_API('Z3_mk_tree_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
      */
-    Z3_ast Z3_API Z3_mk_sr_plo(Z3_context c, Z3_ast a, Z3_ast b);
-
-    /**
-       \brief declare \c a and \c b are in total order.
-
-       \pre a and b are of same type.
-
-       def_API('Z3_mk_sr_to', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
-     */
-    Z3_ast Z3_API Z3_mk_sr_to(Z3_context c, Z3_ast a, Z3_ast b);
+    Z3_ast Z3_API Z3_mk_tree_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
 
     /*@}*/
 
diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp
index b5a55cbb4..6dd0af1b4 100644
--- a/src/ast/special_relations_decl_plugin.cpp
+++ b/src/ast/special_relations_decl_plugin.cpp
@@ -26,7 +26,6 @@ Revision History:
 special_relations_decl_plugin::special_relations_decl_plugin():
     m_lo("linear-order"),
     m_po("partial-order"),
-    m_po_ao("partial-order-already-ordered"),
     m_plo("piecewise-linear-order"),
     m_to("tree-order")
 {}
@@ -47,7 +46,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
     symbol name;
     switch(k) {
     case OP_SPECIAL_RELATION_PO: name = m_po; break;
-    case OP_SPECIAL_RELATION_PO_AO: name = m_po_ao; break;
     case OP_SPECIAL_RELATION_LO: name = m_lo; break;
     case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
     case OP_SPECIAL_RELATION_TO: name = m_to; break;
@@ -58,7 +56,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
 void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     if (logic == symbol::null) {
         op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO));
-        op_names.push_back(builtin_name(m_po_ao.bare_str(), OP_SPECIAL_RELATION_PO_AO));
         op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
         op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
         op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
@@ -68,7 +65,6 @@ void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_name
 sr_property special_relations_util::get_property(func_decl* f) const {
     switch (f->get_decl_kind()) {
     case OP_SPECIAL_RELATION_PO: return sr_po;
-    case OP_SPECIAL_RELATION_PO_AO: return sr_po; // still partial ordered
     case OP_SPECIAL_RELATION_LO: return sr_lo;
     case OP_SPECIAL_RELATION_PLO: return sr_plo;
     case OP_SPECIAL_RELATION_TO: return sr_to;
diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h
index e8260e154..dbdd61805 100644
--- a/src/ast/special_relations_decl_plugin.h
+++ b/src/ast/special_relations_decl_plugin.h
@@ -26,7 +26,6 @@ Revision History:
 enum special_relations_op_kind {
     OP_SPECIAL_RELATION_LO,
     OP_SPECIAL_RELATION_PO,
-    OP_SPECIAL_RELATION_PO_AO,
     OP_SPECIAL_RELATION_PLO,
     OP_SPECIAL_RELATION_TO,
     LAST_SPECIAL_RELATIONS_OP
@@ -35,7 +34,6 @@ enum special_relations_op_kind {
 class special_relations_decl_plugin : public decl_plugin {
     symbol m_lo;
     symbol m_po;
-    symbol m_po_ao;
     symbol m_plo;
     symbol m_to;
 public:
@@ -80,13 +78,11 @@ public:
 
     bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); }
     bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); }
-    bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); }
     bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); }
     bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); }
     
     app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO,  arg1, arg2); }
     app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO,  arg1, arg2); }
-    app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO,  arg1, arg2); }
     app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); }
     app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO,  arg1, arg2); }
 
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index d56844ad9..65d30cea6 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -65,7 +65,11 @@ namespace smt {
     }
 
     std::ostream& theory_special_relations::relation::display(theory_special_relations const& th, std::ostream& out) const {
-        out << m_decl->get_name() << ":\n";
+        out << mk_pp(m_decl, th.get_manager());
+        for (unsigned i = 0; i < m_decl->get_num_parameters(); ++i) {
+            th.get_manager().display(out << " ", m_decl->get_parameter(i));
+        }
+        out << ":\n";
         m_graph.display(out);
         out << "explanation: " << m_explanation << "\n";
         m_uf.display(out);