From 84ed1c19a077a3ef607b427062fa12b26fa80632 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 21 Jan 2015 19:20:43 +0000
Subject: [PATCH] Bugfixes for the Java FPA API

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/java/AST.java  | 12 ++++--------
 src/api/java/Expr.java |  8 ++++++++
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 30d303d6c..0cdfd025c 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -227,10 +227,8 @@ public class AST extends Z3Object
     void incRef(long o) throws Z3Exception
     {
         // Console.WriteLine("AST IncRef()");
-        if (getContext() == null)
-            throw new Z3Exception("inc() called on null context");
-        if (o == 0)
-            throw new Z3Exception("inc() called on null AST");
+        if (getContext() == null || o == 0)
+			return;
         getContext().ast_DRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
@@ -238,10 +236,8 @@ public class AST extends Z3Object
     void decRef(long o) throws Z3Exception
     {
         // Console.WriteLine("AST DecRef()");
-        if (getContext() == null)
-            throw new Z3Exception("dec() called on null context");
-        if (o == 0)
-            throw new Z3Exception("dec() called on null AST");
+        if (getContext() == null || o == 0)
+			return;
         getContext().ast_DRQ().add(o);
         super.decRef(o);
     }
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index f94eb12cb..762a4b672 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -2161,6 +2161,10 @@ public class Expr extends AST
 				return new RatNum(ctx, obj);
 			case Z3_BV_SORT:
 				return new BitVecNum(ctx, obj);
+			case Z3_FLOATING_POINT_SORT:
+				return new FPNum(ctx, obj);
+			case Z3_ROUNDING_MODE_SORT:
+				return new FPRMNum(ctx, obj);
 			default: ;
 			}
 		}
@@ -2179,6 +2183,10 @@ public class Expr extends AST
 			return new ArrayExpr(ctx, obj);
 		case Z3_DATATYPE_SORT:
 			return new DatatypeExpr(ctx, obj);
+		case Z3_FLOATING_POINT_SORT:
+			return new FPExpr(ctx, obj);
+		case Z3_ROUNDING_MODE_SORT:
+			return new FPRMExpr(ctx, obj);
 		default: ;
 		}