Minor Changes

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java

@@ -27,9 +27,6 @@ private record Substitution(VCImplication node, Expression replacement) {
      */
     @Override
     public VCImplication apply(VCImplication implication) {
-        if (implication == null)
-            return null;
-
         VCImplication result = implication.clone();
         Optional<VCSubstitution.Substitution> substitutionOpt = findSubstitution(result);
 

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java

@@ -3,7 +3,6 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertInstanceOf;
-import static org.junit.jupiter.api.Assertions.assertNull;
 
 import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
@@ -13,11 +12,6 @@ class VCArithmeticSimplificationTest {
 
     private final VCArithmeticSimplification simplification = new VCArithmeticSimplification();
 
-    @Test
-    void applyReturnsNullForNullImplication() {
-        assertNull(simplification.apply(null));
-    }
-
     @Test
     void simplifiesAdditiveIdentities() {
         assertSimplificationSteps(simplification::apply, vc("x + 0 > 0"), chain(expect("x > 0", "x + 0 > 0")));

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java

@@ -3,7 +3,6 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertInstanceOf;
-import static org.junit.jupiter.api.Assertions.assertNull;
 
 import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
@@ -18,11 +17,6 @@ class VCFoldingTest {
 
     private final VCFolding folding = new VCFolding();
 
-    @Test
-    void applyReturnsNullForNullImplication() {
-        assertNull(folding.apply(null));
-    }
-
     @Test
     void foldsIntegerArithmeticAndComparisons() {
         VCImplication implication = vc("1 + 2 == 3");

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java

@@ -3,7 +3,6 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertInstanceOf;
-import static org.junit.jupiter.api.Assertions.assertNull;
 
 import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
@@ -13,11 +12,6 @@ class VCLogicalSimplificationTest {
 
     private final VCLogicalSimplification simplification = new VCLogicalSimplification();
 
-    @Test
-    void applyReturnsNullForNullImplication() {
-        assertNull(simplification.apply(null));
-    }
-
     @Test
     void simplifiesConjunctionWithBooleanLiterals() {
         assertSimplificationSteps(simplification::apply, vc("x && true"), chain(expect("x", "x && true")));

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java

@@ -1,7 +1,6 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.utils.VCTestUtils.*;
-import static org.junit.jupiter.api.Assertions.assertNull;
 
 import liquidjava.processor.VCImplication;
 import org.junit.jupiter.api.Test;
@@ -10,11 +9,6 @@ class VCSubstitutionTest {
 
     private final VCSubstitution substitution = new VCSubstitution();
 
-    @Test
-    void applyReturnsNullForNullImplication() {
-        assertNull(substitution.apply(null));
-    }
-
     @Test
     void substitutesBinderEqualityIntoWholeChain() {
         VCImplication implication = vc("∀x:int. x == 3", "x > 0");