Drop the bare true row left at the end of Found

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

@@ -57,8 +57,17 @@ private VCImplication simplify(VCImplication implication, Set<String> keptTrueBi
         if (next == null)
             return null;
 
+        return withNext(implication, next);
+    }
+
+    /**
+     * Copies a VC node followed by its simplified suffix, leaving out a suffix that became just true
+     */
+    private VCImplication withNext(VCImplication implication, VCImplication next) {
         VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
-        result.setNext(next);
+        // Found reads its rows as a conjunction, so P && true -> P: a trailing true row only reads as the value above
+        if (!isPlainTrue(next))
+            result.setNext(next);
         return result;
     }
 
@@ -119,6 +128,14 @@ private boolean isTrueBinder(VCImplication implication) {
         return implication.hasBinder() && isTrue(implication.getRefinement().getExpression());
     }
 
+    /**
+     * Checks whether a VC node is a last implication without binder refined with true
+     */
+    private boolean isPlainTrue(VCImplication implication) {
+        return !implication.hasBinder() && !implication.hasNext()
+                && isTrue(implication.getRefinement().getExpression());
+    }
+
     /**
      * Checks whether a VC node is a binder refined with false
      */

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

@@ -104,6 +104,22 @@ void ignoresNonBinderBooleanLiterals() {
         assertSimplificationSteps(binderSimplification, vc("true", "false"), step("true", "false"));
     }
 
+    @Test
+    void removesLastTrueBinderWithoutLeavingTrue() {
+        assertSimplificationSteps(binderSimplification, vc("∀p:boolean. p || q", "∀x:Object. true"), step("p || q"));
+    }
+
+    @Test
+    void removesLastTrueBinderAfterNestedConditionsWithoutLeavingTrue() {
+        assertSimplificationSteps(binderSimplification, vc("∀p:boolean. p", "∀q:boolean. !q", "∀x:Object. true"),
+                step("p", "!q"));
+    }
+
+    @Test
+    void collapsedFalseBinderLeavesNoTrueAfterAnotherRow() {
+        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "∀y:int. false", "z > 0"), step("x > 0"));
+    }
+
     @Test
     void trueBinderWithoutSuffixBecomesPlainTrue() {
         assertSimplificationSteps(binderSimplification, vc("∀x:int. true"), step("true"));