diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 1cee7469c..d3dabcd4e 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -235,7 +235,7 @@ extern "C" { expr* e = to_expr(a); if (!e) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(""); + return ""; } rational r; arith_util & u = mk_c(c)->autil();