From c350943c783c8bf23148f2ec88130e69252e64d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Dec 2012 15:59:54 -0800 Subject: [PATCH] fixed bug introduced today Signed-off-by: Leonardo de Moura --- src/api/api_ast.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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; }