From 7255a2afd1cf5896dba2e49cd3a570760ad5fa71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jul 2021 18:43:11 +0200 Subject: [PATCH] fix #5379 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d16295418..cf650a5fa 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4620,8 +4620,9 @@ extern "C" { /** \brief Return a hash code for the given AST. - The hash code is structural. You can use Z3_get_ast_id interchangeably with - this function. + The hash code is structural but two different AST objects can map to the same hash. + The result of \c Z3_get_ast_id returns an indentifier that is unique over the + set of live AST objects. def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST))) */