From b93ffe676be77fe0ac2846d79b9e1a00c7837ba1 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 20 Nov 2018 11:34:32 +0700 Subject: [PATCH 1/2] Fix broken link. It is Z3_add_rec_def, not Z3_mk_rec_def. --- src/api/z3_api.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index a94030d22..e78dacbcb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2154,12 +2154,12 @@ extern "C" { \param domain array containing the sort of each argument. The array must contain domain_size elements. \param range sort of the constant or the return sort of the function. - After declaring recursive function, it should be associated with a recursive definition #Z3_mk_rec_def. + After declaring recursive function, it should be associated with a recursive definition #Z3_add_rec_def. The function #Z3_mk_app can be used to create a constant or function application. \sa Z3_mk_app - \sa Z3_mk_rec_def + \sa Z3_add_rec_def def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) */ From 67ea2a2c88ae804b4a276cddf65d123f401c833b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 20 Nov 2018 09:52:43 -0800 Subject: [PATCH 2/2] test Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/util/lp/gomory.h b/src/util/lp/gomory.h index b7946d6b0..acb5f04fd 100644 --- a/src/util/lp/gomory.h +++ b/src/util/lp/gomory.h @@ -14,8 +14,6 @@ Author: Lev Nachmanson (levnach) Revision History: - - --*/ #pragma once #include "util/lp/lar_term.h"