mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
Java API: bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
67485b8af7
commit
eb3fa254d8
|
@ -37,13 +37,15 @@ public class AST extends Z3Object
|
|||
**/
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
AST casted = null;
|
||||
AST casted = null;
|
||||
|
||||
try {
|
||||
casted = AST.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
try
|
||||
{
|
||||
casted = AST.class.cast(o);
|
||||
} catch (ClassCastException e)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
return this.NativeObject() == casted.NativeObject();
|
||||
}
|
||||
|
@ -60,18 +62,20 @@ public class AST extends Z3Object
|
|||
return 1;
|
||||
|
||||
AST oAST = null;
|
||||
try {
|
||||
AST.class.cast(other);
|
||||
} catch (ClassCastException e) {
|
||||
return 1;
|
||||
}
|
||||
try
|
||||
{
|
||||
oAST = AST.class.cast(other);
|
||||
} catch (ClassCastException e)
|
||||
{
|
||||
return 1;
|
||||
}
|
||||
|
||||
if (Id() < oAST.Id())
|
||||
return -1;
|
||||
else if (Id() > oAST.Id())
|
||||
return +1;
|
||||
else
|
||||
return 0;
|
||||
if (Id() < oAST.Id())
|
||||
return -1;
|
||||
else if (Id() > oAST.Id())
|
||||
return +1;
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
Loading…
Reference in a new issue