Open
Description
On c503366 (current test-gen-support), CBMC is able to verify the first assert
, but fails to verify the second. As the only difference between the two asserts
is the known type information at each point, it seems likely that CBMC is unable to resolve the correct equals
to call.
public class equals_Pass {
private static boolean myEquals(Object a, Object b) {
return (a == b) || (a != null && a.equals(b));
}
public static void main(String[] args) {
String a = new String("abc");
String b = new String("abc");
assert((a == b) || (a != null && a.equals(b)));
boolean result = myEquals(a, b);
assert(result);
}
}