From e1572096ca707c58f7cb91337dfba71d4d9f4592 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 7 Feb 2021 12:14:52 +0000 Subject: [PATCH] delete some dead code --- src/api/api_model.cpp | 37 ------------------------------------- src/api/api_stats.cpp | 1 - 2 files changed, 38 deletions(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index a4c0cfec1..1fd9ad1f9 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -422,44 +422,7 @@ extern "C" { expr * r = to_func_entry(e)->m_func_entry->get_arg(i); RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(nullptr); - } - - unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) { - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, 0); - Z3_func_decl d = get_model_func_decl_core(c, m, i); - if (d) { - model * _m = to_model_ref(m); - func_interp * g = _m->get_func_interp(to_func_decl(d)); - if (g) { - return g->num_entries(); - } - SET_ERROR_CODE(Z3_IOB, nullptr); - return 0; - } - return 0; } - - - unsigned get_model_func_entry_num_args_core(Z3_context c, - Z3_model m, - unsigned i, - unsigned j) { - RESET_ERROR_CODE(); - CHECK_NON_NULL(m, 0); - if (j >= get_model_func_num_entries_core(c, m, i)) { - SET_ERROR_CODE(Z3_IOB, nullptr); - return 0; - } - Z3_func_decl d = get_model_func_decl_core(c, m, i); - if (d) { - model * _m = to_model_ref(m); - func_interp * g = _m->get_func_interp(to_func_decl(d)); - return g->get_arity(); - } - return 0; - } - Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) { Z3_TRY; diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index 410118c9d..0278d7d31 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -31,7 +31,6 @@ extern "C" { to_stats_ref(s).display_smt2(buffer); std::string result = buffer.str(); // Hack for removing the trailing '\n' - result = buffer.str(); SASSERT(result.size() > 0); result.resize(result.size()-1); return mk_c(c)->mk_external_string(std::move(result));