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: ; }