mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-11-20 10:29:03 -08:00
parent 5a94cece2e 67ea2a2c88
commit 656cdc4635
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/z3_api.h
View file

@ -2154,12 +2154,12 @@ extern "C" {
\param domain array containing the sort of each argument. The array must contain domain_size elements. \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. \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 The function #Z3_mk_app can be used to create a constant or function
application. application.
\sa Z3_mk_app \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))) def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
*/ */

2
src/util/lp/gomory.h
View file

@ -14,8 +14,6 @@ Author:
Lev Nachmanson (levnach) Lev Nachmanson (levnach)
Revision History: Revision History:
--*/ --*/
#pragma once #pragma once
#include "util/lp/lar_term.h" #include "util/lp/lar_term.h"