diff --git a/src/api/api_context.h b/src/api/api_context.h index de492bb45..fa6754120 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,7 +58,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; - datatype_util m_dtutil; + datatype_util m_dtutil; seq_util m_sutil; // Support for old solver API @@ -67,7 +67,6 @@ namespace api { ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false - unsigned_vector m_ast_lim; ref m_last_obj; //!< reference to the last API object returned by the APIs @@ -122,7 +121,7 @@ namespace api { bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } - datatype_util& dtutil() { return m_dtutil; } + datatype_util& dtutil() { return m_dtutil; } seq_util& sutil() { return m_sutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } @@ -180,8 +179,6 @@ namespace api { void interrupt(); void invoke_error_handler(Z3_error_code c); - - static void out_of_memory_handler(void * _ctx); void check_sorts(ast * n);