From 02d6f6a613bbd5dd7b53d77672ca1c756c21b96e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Apr 2022 10:01:51 +0100 Subject: [PATCH] fix build for Z3_mk_datatype_sort Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 23ff21575..f1c65b626 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -370,9 +370,9 @@ extern "C" { LOG_Z3_mk_datatype_sort(c, name); RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); - datatype_util data_util(m); - parameter param(name); - sort * s = m.mk_sort(util.get_family_id(), DATATYPE_SORT, 1, ¶m); + datatype_util adt_util(m); + parameter p(to_symbol(name)); + sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p); mk_c(c)->save_ast_trail(s); RETURN_Z3(of_sort(s)); Z3_CATCH_RETURN(nullptr);