mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
parent
6263252bf5
commit
e312b47be6
|
@ -33,7 +33,7 @@ public class AST extends Z3Object implements Comparable
|
||||||
{
|
{
|
||||||
AST casted = null;
|
AST casted = null;
|
||||||
|
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
casted = AST.class.cast(o);
|
casted = AST.class.cast(o);
|
||||||
} catch (ClassCastException e)
|
} catch (ClassCastException e)
|
||||||
|
@ -41,13 +41,12 @@ public class AST extends Z3Object implements Comparable
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
return
|
return (this == casted) ||
|
||||||
(this == casted) ||
|
(this != null) &&
|
||||||
(this != null) &&
|
(casted != null) &&
|
||||||
(casted != null) &&
|
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
(Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
||||||
(Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
}
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Object Comparison.
|
* Object Comparison.
|
||||||
|
|
|
@ -80,11 +80,20 @@ public class Constructor extends Z3Object
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Destructor.
|
* Destructor.
|
||||||
|
* @throws Throwable
|
||||||
* @throws Z3Exception on error
|
* @throws Z3Exception on error
|
||||||
**/
|
**/
|
||||||
protected void finalize()
|
protected void finalize() throws Throwable
|
||||||
{
|
{
|
||||||
Native.delConstructor(getContext().nCtx(), getNativeObject());
|
try {
|
||||||
|
Native.delConstructor(getContext().nCtx(), getNativeObject());
|
||||||
|
}
|
||||||
|
catch (Throwable t) {
|
||||||
|
throw t;
|
||||||
|
}
|
||||||
|
finally {
|
||||||
|
super.finalize();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private int n = 0;
|
private int n = 0;
|
||||||
|
|
|
@ -24,11 +24,20 @@ public class ConstructorList extends Z3Object
|
||||||
{
|
{
|
||||||
/**
|
/**
|
||||||
* Destructor.
|
* Destructor.
|
||||||
|
* @throws Throwable
|
||||||
* @throws Z3Exception on error
|
* @throws Z3Exception on error
|
||||||
**/
|
**/
|
||||||
protected void finalize()
|
protected void finalize() throws Throwable
|
||||||
{
|
{
|
||||||
Native.delConstructorList(getContext().nCtx(), getNativeObject());
|
try {
|
||||||
|
Native.delConstructorList(getContext().nCtx(), getNativeObject());
|
||||||
|
}
|
||||||
|
catch (Throwable t) {
|
||||||
|
throw t;
|
||||||
|
}
|
||||||
|
finally {
|
||||||
|
super.finalize();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
ConstructorList(Context ctx, long obj)
|
ConstructorList(Context ctx, long obj)
|
||||||
|
|
|
@ -25,10 +25,19 @@ public class Z3Object extends IDisposable
|
||||||
{
|
{
|
||||||
/**
|
/**
|
||||||
* Finalizer.
|
* Finalizer.
|
||||||
|
* @throws Throwable
|
||||||
**/
|
**/
|
||||||
protected void finalize()
|
protected void finalize() throws Throwable
|
||||||
{
|
{
|
||||||
dispose();
|
try {
|
||||||
|
dispose();
|
||||||
|
}
|
||||||
|
catch (Throwable t) {
|
||||||
|
throw t;
|
||||||
|
}
|
||||||
|
finally {
|
||||||
|
super.finalize();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
|
Loading…
Reference in a new issue