Add Tests

Author: rcosta358

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

@@ -96,6 +96,21 @@ void simplifiesOnlyFirstArithmeticIdentity() {
                 chain(expect("x + 1 > 0", "x + 0 + 1 > 0")));
     }
 
+    @Test
+    void simplifiesTernaryExpressionsInConditionThenElseOrder() {
+        assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(flag + 0 > 0 ? x + 0 : y + 0) > 0"),
+                chain(expect("(flag > 0 ? x + 0 : y + 0) > 0", "(flag + 0 > 0 ? x + 0 : y + 0) > 0")),
+                chain(expect("(flag > 0 ? x : y + 0) > 0", "(flag > 0 ? x + 0 : y + 0) > 0")),
+                chain(expect("(flag > 0 ? x : y) > 0", "(flag > 0 ? x : y + 0) > 0")));
+    }
+
+    @Test
+    void simplifiesGroupedExpressionsAndLeavesUnchangedGroupsAlone() {
+        assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x + 0) * y > 0"),
+                chain(expect("x * y > 0", "(x + 0) * y > 0")));
+        assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x) > 0"), chain(expect("x > 0", "x > 0")));
+    }
+
     @Test
     void recordsOriginWhenSimplifyingLaterImplication() {
         VCImplication implication = vc("x > 0", "y + 0 > x");