From 95d7b33ebb2e27e85cc49d8490b3593c1b2e7ec7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 27 Oct 2016 15:07:10 +0100
Subject: [PATCH] Added is_numeral_negative to .NET and Java APIs

---
 src/api/dotnet/FPNum.cs |  5 +++++
 src/api/java/FPNum.java | 11 +++++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs
index 05eda00b3..808752eaa 100644
--- a/src/api/dotnet/FPNum.cs
+++ b/src/api/dotnet/FPNum.cs
@@ -166,6 +166,11 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
 
+        /// <summary>
+        /// Indicates whether the numeral is negative.
+        /// </summary>
+        public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
+
         #region Internal
         internal FPNum(Context ctx, IntPtr obj)
             : base(ctx, obj)
diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java
index a8f8af4ff..813e82889 100644
--- a/src/api/java/FPNum.java
+++ b/src/api/java/FPNum.java
@@ -166,6 +166,17 @@ public class FPNum extends FPExpr
     {
         return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
     }
+
+    /**
+     * Indicates whether the numeral is negative.
+     * @throws Z3Exception on error
+     * @return a boolean
+     **/
+    public boolean isNegative()
+    {
+        return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
+    }
+
     
     public FPNum(Context ctx, long obj)
     {