Skip to content

Commit f5cccb1

Browse files
committed
Assert Origin Not Equal to Simplified
1 parent 9e76dcf commit f5cccb1

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22

33
import static org.junit.jupiter.api.Assertions.assertEquals;
44
import static org.junit.jupiter.api.Assertions.assertNotNull;
5+
import static org.junit.jupiter.api.Assertions.assertNotEquals;
6+
import static org.junit.jupiter.api.Assertions.assertNotSame;
57
import static org.junit.jupiter.api.Assertions.assertNull;
68

79
import liquidjava.processor.VCImplication;
@@ -59,6 +61,9 @@ private static void assertSimplificationResult(VCSimplificationResult previous,
5961
assertNull(result.getOrigin(), "Unchanged simplification result should not have an origin");
6062
} else {
6163
assertNotNull(result.getOrigin(), "Changed simplification result should have an origin");
64+
assertNotSame(result, result.getOrigin(), "Simplification result should not be its own origin");
65+
assertNotEquals(result.getImplication(), result.getOrigin().getImplication(),
66+
"Simplification origin should differ from the simplified VC");
6267
assertEquals(previous.getImplication(), result.getOrigin().getImplication(),
6368
"Simplification origin should be the complete previous VC");
6469
}

0 commit comments

Comments
 (0)