mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity

Remove unnecessary pre-condition.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-04-09 08:56:01 -07:00
parent 806fc68fa5
commit 8e20b3f248
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/z3_api.h
View file

@ -4515,9 +4515,7 @@ END_MLAPI_EXCLUDE
Z3_ast_opt Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
/**
\brief Test if there exists an interpretation (i.e., assignment) of constant \c a in the model \c m.
\pre Z3_get_arity(c, a) == 0
\brief Test if there exists an interpretation (i.e., assignment) for \c a in the model \c m.
def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
*/