Minor Improvements

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -38,7 +38,7 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica
 
     @Override
     public String getDetails() {
-        if (counterexample == null)
+        if (counterexample.isEmpty())
             return "";
 
         String counterexampleString = counterexample.assignments().stream()
@@ -61,9 +61,6 @@ public VCSimplificationResult getFound() {
 
     // Filters counterexample assignments only in found VC and sorts them in the order of its binders
     private Counterexample filterCounterexample(Counterexample counterexample) {
-        if (counterexample == null || counterexample.assignments().isEmpty())
-            return null;
-
         List<String> binderNames = getFound().getBinders();
         Set<String> knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream()
                 .map(Expression::toString).collect(Collectors.toSet());
@@ -73,9 +70,6 @@ private Counterexample filterCounterexample(Counterexample counterexample) {
                 .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first())))
                 .toList();
 
-        if (assignments.isEmpty())
-            return null;
-
         return new Counterexample(assignments);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java

@@ -5,4 +5,7 @@
 import liquidjava.utils.Pair;
 
 public record Counterexample(List<Pair<String, String>> assignments) {
+    public boolean isEmpty() {
+        return assignments.isEmpty();
+    }
 }