mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
various partial fixes for issue #143
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9dd704bc4b
commit
ade9b2830a
3 changed files with 26 additions and 8 deletions
|
@ -47,9 +47,14 @@ public class FuncDecl extends AST
|
|||
**/
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
FuncDecl casted = (FuncDecl) o;
|
||||
if (casted == null)
|
||||
FuncDecl casted = null;
|
||||
|
||||
try {
|
||||
casted = FuncDecl.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
}
|
||||
|
||||
|
|
|
@ -36,13 +36,13 @@ public class Sort extends AST
|
|||
{
|
||||
Sort casted = null;
|
||||
|
||||
try {
|
||||
casted = Sort.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
try {
|
||||
casted = Sort.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
@ -49,6 +49,19 @@ public class Symbol extends Z3Object
|
|||
return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
|
||||
}
|
||||
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
Symbol casted = null;
|
||||
try {
|
||||
casted = Symbol.class.cast(o);
|
||||
}
|
||||
catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
}
|
||||
|
||||
/**
|
||||
* A string representation of the symbol.
|
||||
**/
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue