-
Notifications
You must be signed in to change notification settings - Fork 19
Open
Description
Hello everyone,
in SMTInterpol two Bitvector constants only seem to be equal only when they were created from the same String object:
@Test
public void testBinary() {
Theory theory = new Theory(Logics.QF_BV);
Term b1 = theory.binary("#b1111");
Term b2 = theory.binary("#b1111");
assertThat(b1).isEqualTo(b1); // Works
assertThat(b1).isEqualTo(b2); // Fails
}
@Test
public void testHexadecimal() {
Theory theory = new Theory(Logics.QF_BV);
Term h1 = theory.hexadecimal("#xf");
Term h2 = theory.hexadecimal("#xf");
assertThat(h1).isEqualTo(h1); // Works
assertThat(h1).isEqualTo(h2); // Fails
}
This is somewhat surprising as the same Test does work for reals:
@Test
public void testDecimal() {
Theory theory = new Theory(Logics.QF_LRA);
Term d1 = theory.decimal("0.1");
Term d2 = theory.decimal("0.1");
assertThat(d1).isEqualTo(d1); // Works
assertThat(d1).isEqualTo(d2); // Also works
}
Could this be fixes so that Bitvector constants are considered equal when their String representation is equal?
Metadata
Metadata
Assignees
Labels
No labels