mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 19:36:17 +00:00
Code Activity

fix build for Z3_mk_datatype_sort

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-27 10:01:51 +01:00
parent 81d97a81af
commit 02d6f6a613
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_datatype.cpp
View file

@ -370,9 +370,9 @@ extern "C" {
LOG_Z3_mk_datatype_sort(c, name); LOG_Z3_mk_datatype_sort(c, name);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
datatype_util data_util(m); datatype_util adt_util(m);
parameter param(name); parameter p(to_symbol(name));
sort * s = m.mk_sort(util.get_family_id(), DATATYPE_SORT, 1, &param); sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p);
mk_c(c)->save_ast_trail(s); mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s)); RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);