From 5d0be96fd1139442bffaedd2cb3ea5415e5ddb11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jan 2026 09:22:43 -0800 Subject: [PATCH] update RCFNum Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/RCFNum.cs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/dotnet/RCFNum.cs b/src/api/dotnet/RCFNum.cs index 3730cbf55..5231632b0 100644 --- a/src/api/dotnet/RCFNum.cs +++ b/src/api/dotnet/RCFNum.cs @@ -248,7 +248,7 @@ namespace Microsoft.Z3 public bool Lt(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_lt(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_lt(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -259,7 +259,7 @@ namespace Microsoft.Z3 public bool Gt(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_gt(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_gt(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -270,7 +270,7 @@ namespace Microsoft.Z3 public bool Le(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_le(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_le(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -281,7 +281,7 @@ namespace Microsoft.Z3 public bool Ge(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_ge(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_ge(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -292,7 +292,7 @@ namespace Microsoft.Z3 public bool Eq(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_eq(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_eq(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -303,7 +303,7 @@ namespace Microsoft.Z3 public bool Neq(RCFNum other) { CheckContext(other); - return Native.Z3_rcf_neq(Context.nCtx, NativeObject, other.NativeObject); + return 0 != Native.Z3_rcf_neq(Context.nCtx, NativeObject, other.NativeObject); } /// @@ -362,7 +362,7 @@ namespace Microsoft.Z3 /// true if this is rational public bool IsRational() { - return Native.Z3_rcf_is_rational(Context.nCtx, NativeObject); + return 0 != Native.Z3_rcf_is_rational(Context.nCtx, NativeObject); } /// @@ -371,7 +371,7 @@ namespace Microsoft.Z3 /// true if this is algebraic public bool IsAlgebraic() { - return Native.Z3_rcf_is_algebraic(Context.nCtx, NativeObject); + return 0 != Native.Z3_rcf_is_algebraic(Context.nCtx, NativeObject); } /// @@ -380,7 +380,7 @@ namespace Microsoft.Z3 /// true if this is infinitesimal public bool IsInfinitesimal() { - return Native.Z3_rcf_is_infinitesimal(Context.nCtx, NativeObject); + return 0 != Native.Z3_rcf_is_infinitesimal(Context.nCtx, NativeObject); } /// @@ -389,7 +389,7 @@ namespace Microsoft.Z3 /// true if this is transcendental public bool IsTranscendental() { - return Native.Z3_rcf_is_transcendental(Context.nCtx, NativeObject); + return 0 != Native.Z3_rcf_is_transcendental(Context.nCtx, NativeObject); } ///