diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 385035361..89c0814f7 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -1615,7 +1615,7 @@ void error_code_example2() { Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1803,7 +1803,7 @@ void parser_example5() { Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg_ex(ctx, (Z3_error_code)r)); + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); del_solver(ctx, s); diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 6c355a4a9..2773b6cc9 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -2209,7 +2209,7 @@ static bool is_smt2_file(char const* filename) { static void check_error(z3::context& ctx) { Z3_error_code e = Z3_get_error_code(ctx); if (e != Z3_OK) { - std::cout << Z3_get_error_msg_ex(ctx, e) << "\n"; + std::cout << Z3_get_error_msg(ctx, e) << "\n"; exit(1); } }