diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index c604927fd..404d9d9ac 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -324,7 +324,8 @@ extern "C" {
         switch (_a->get_kind()) {
         case AST_APP: {
             expr * e = to_expr(_a);
-            if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_value(e)) 
+            // Real algebraic numbers are not considered Z3_NUMERAL_AST
+            if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e)) 
                 return Z3_NUMERAL_AST;
             return Z3_APP_AST;
         }