mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
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>
This commit is contained in:
parent
42162f1ea5
commit
84ed1c19a0
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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: ;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue