diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index a79f55855..cc1ccf59e 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -121,7 +121,9 @@ extern "C" { Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { LOG_Z3_is_algebraic_number(c, a); - return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)); + Z3_bool r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? Z3_TRUE : Z3_FALSE; + IF_VERBOSE(10, verbose_stream() << r << "\n"); + return r; } Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 99745ffff..1e0f495f5 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1822,7 +1822,7 @@ namespace Microsoft.Z3 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); - if (Z3_sort_kind.Z3_REAL_SORT == sk && + if ( // Z3_sort_kind.Z3_REAL_SORT == sk && Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj);