From 1ae0a9813251cb7fb9a966664fd8f15902d7f958 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Aug 2019 13:37:22 -0700 Subject: [PATCH] fix #2466 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index c7d50af7c..0773bdb94 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3674,10 +3674,8 @@ extern "C" { /** @name Special relations */ /*@{*/ /** - \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. - + \brief create a linear ordering relation over signature \c a. + The relation is identified by the index \c id. def_API('Z3_mk_linear_order', FUNC_DECL ,(_in(CONTEXT), _in(SORT), _in(UINT))) */