From 56db84a0e5a802238c0f43b85eeca8679eafbd55 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Jan 2013 15:10:16 -0800
Subject: [PATCH] Fix RCF API logging bug

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/api/api_rcf.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
     }