diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 5c76adfad..c79dfbf20 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -133,7 +133,7 @@ extern "C" { for (unsigned i = 0; i < num_roots; i++) { roots[i] = from_rcnumeral(rs[i]); } - return num_roots; + RETURN_Z3_rcf_mk_roots num_roots; Z3_CATCH_RETURN(0); }