From cbfc085d4a11412717d42014393c3035cc89242a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 14 Jul 2026 19:48:25 +0100 Subject: [PATCH 1/6] Filter & Sort Counterexamples by Binders --- .../diagnostics/errors/RefinementError.java | 37 +++++++------------ .../opt/VCSimplificationResult.java | 13 +++++++ 2 files changed, 27 insertions(+), 23 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 78b5e0aa..ee9bf0f7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -7,7 +7,6 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; @@ -38,38 +37,30 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica @Override public String getDetails() { - String counterexampleString = getCounterExampleString(); - if (counterexampleString == null) + Counterexample counterexamples = getCounterExamples(); + if (counterexamples == null) return ""; + + String counterexampleString = counterexamples.assignments().stream() + .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) + .collect(Collectors.joining(" && ")); return "Counterexample: " + counterexampleString; } - public String getCounterExampleString() { + // Filters counterexample assignments only in found VC and sorts them in the order of its binders + public Counterexample getCounterExamples() { if (counterexample == null || counterexample.assignments().isEmpty()) return null; - List foundVarNames = new ArrayList<>(); - Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); - Expression expectedExpression = expected.getExpression(); - foundExpression.getVariableNames(foundVarNames); - // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the - // subtyping check, so the counterexample maps the symbolic name back to its compile-time value - foundExpression.getResolvedConstantNames(foundVarNames); - expectedExpression.getResolvedConstantNames(foundVarNames); - List foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList(); - String counterexampleString = counterexample.assignments().stream() - // only include variables that appear in the found value and are not already fixed there - .filter(a -> foundVarNames.contains(a.first()) - && !foundAssignments.contains(a.first() + " == " + a.second())) - // format as "var == value" - .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) - // join with "&&" - .collect(Collectors.joining(" && ")); + List binderNames = getFound().getBinders(); + var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) + .toList(); - if (counterexampleString.isEmpty()) + if (assignments.isEmpty()) return null; - return counterexampleString; + return new Counterexample(assignments); } public Counterexample getCounterexample() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index 6f35822d..8fe00a84 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -1,5 +1,7 @@ package liquidjava.rj_language.opt; +import java.util.ArrayList; +import java.util.List; import java.util.Objects; import liquidjava.processor.VCImplication; @@ -46,6 +48,17 @@ public String getSimplification() { return simplification; } + /** + * Returns the list of binder names in the simplified VC chain in order of appearance + */ + public List getBinders() { + ArrayList binderNames = new ArrayList<>(); + for (VCImplication current = getImplication(); current != null; current = current.getNext()) + if (current.hasBinder()) + binderNames.add(current.getName()); + return binderNames; + } + @Override public String toString() { if (origin == null) From eaf483e0a6092291e99cfe3146f534e014e177b4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 14 Jul 2026 21:01:36 +0100 Subject: [PATCH 2/6] Filter Known Assignments --- .../liquidjava/diagnostics/errors/RefinementError.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index ee9bf0f7..433e26ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,12 +1,12 @@ package liquidjava.diagnostics.errors; -import java.util.ArrayList; import java.util.List; +import java.util.Set; import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; @@ -53,7 +53,10 @@ public Counterexample getCounterExamples() { return null; List binderNames = getFound().getBinders(); + Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() + .map(Expression::toString).collect(Collectors.toSet()); var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) .toList(); From 6e76a26609abae69346a7d82c7c91b717bbe2400 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 15:48:52 +0100 Subject: [PATCH 3/6] Refactor Counterexamples --- .../diagnostics/errors/RefinementError.java | 37 ++++++++++--------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 433e26ea..28f38881 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -10,6 +10,7 @@ import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; import spoon.reflect.cu.SourcePosition; /** @@ -32,30 +33,42 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica position, translationTable, customMessage); this.expected = expected; this.found = found; - this.counterexample = counterexample; + this.counterexample = filterCounterexample(counterexample); } @Override public String getDetails() { - Counterexample counterexamples = getCounterExamples(); - if (counterexamples == null) + if (counterexample == null) return ""; - String counterexampleString = counterexamples.assignments().stream() + String counterexampleString = counterexample.assignments().stream() .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) .collect(Collectors.joining(" && ")); return "Counterexample: " + counterexampleString; } + public Counterexample getCounterexample() { + return counterexample; + } + + public Predicate getExpected() { + return expected; + } + + public VCSimplificationResult getFound() { + return found; + } + // Filters counterexample assignments only in found VC and sorts them in the order of its binders - public Counterexample getCounterExamples() { + private Counterexample filterCounterexample(Counterexample counterexample) { if (counterexample == null || counterexample.assignments().isEmpty()) return null; List binderNames = getFound().getBinders(); Set knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream() .map(Expression::toString).collect(Collectors.toSet()); - var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first())) + List> assignments = counterexample.assignments().stream() + .filter(a -> binderNames.contains(a.first())) .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second())) .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first()))) .toList(); @@ -65,16 +78,4 @@ public Counterexample getCounterExamples() { return new Counterexample(assignments); } - - public Counterexample getCounterexample() { - return counterexample; - } - - public Predicate getExpected() { - return expected; - } - - public VCSimplificationResult getFound() { - return found; - } } From bcaea90f847e0fe88a94630b9e99d70aa3d005fc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 17:48:59 +0100 Subject: [PATCH 4/6] Minor Improvements --- .../liquidjava/diagnostics/errors/RefinementError.java | 8 +------- .../src/main/java/liquidjava/smt/Counterexample.java | 3 +++ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 28f38881..e258425a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/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 binderNames = getFound().getBinders(); Set 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); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java index 3d72973e..93820e05 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java @@ -5,4 +5,7 @@ import liquidjava.utils.Pair; public record Counterexample(List> assignments) { + public boolean isEmpty() { + return assignments.isEmpty(); + } } From 98c485ede1a15c1fb8ee3fb04d1e25f871d3dd35 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 18:14:48 +0100 Subject: [PATCH 5/6] Add Counterexample Tests --- .../src/main/java/testSuite/ErrorBoolean.java | 11 ++ .../testSuite/ErrorDependentRefinement.java | 2 +- .../testSuite/ErrorDependentUpperBound.java | 13 +++ .../main/java/testSuite/ErrorIdentity.java | 11 ++ .../java/testSuite/ErrorIntegerDivision.java | 11 ++ .../main/java/testSuite/ErrorLiteralZero.java | 11 ++ .../testSuite/ErrorRecursiveDecrement.java | 10 ++ .../api/tests/TestCounterexamples.java | 104 ++++++++++++++++++ 8 files changed, 172 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoolean.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIdentity.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java new file mode 100644 index 00000000..486ab222 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoolean.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorBoolean { + + @Refinement("_ == true") + boolean mustBeTrue(boolean value) { + return value; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java index 42f18673..d593bc62 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java @@ -9,7 +9,7 @@ public static void main(String[] args) { int smaller = 5; @Refinement("bigger > 20") int bigger = 50; - @Refinement("_ > smaller && _ < bigger") + @Refinement("_ > smaller && _ < bigger") int middle = 21; // Refinement Error } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java new file mode 100644 index 00000000..0310089a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentUpperBound.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorDependentUpperBound { + + @Refinement("0 <= _ && _ < len") + int nextIndex( + @Refinement("_ > 0") int len, + @Refinement("0 <= _ && _ < len") int i) { + return i + 1; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java new file mode 100644 index 00000000..a88c8091 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIdentity.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorIdentity { + + @Refinement("_ > 0") + int positiveIdentity(int x) { + return x; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java new file mode 100644 index 00000000..6f6e616c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIntegerDivision.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorIntegerDivision { + + @Refinement("_ > 0") + int half(@Refinement("_ > 0") int x) { + return x / 2; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java new file mode 100644 index 00000000..8490425a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLiteralZero.java @@ -0,0 +1,11 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLiteralZero { + + @Refinement("_ != 0") + int zero() { + return 0; // Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java new file mode 100644 index 00000000..a9477c97 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursiveDecrement.java @@ -0,0 +1,10 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorRecursiveDecrement { + + public int f(@Refinement("_ > 0") int x) { + return f(x - 1); // Refinement Error + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java new file mode 100644 index 00000000..77fb3692 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -0,0 +1,104 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.utils.Pair; + +class TestCounterexamples { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + + @Test + void recursiveDecrementIncludesInputAndGeneratedArgument() { + RefinementError error = verify("ErrorRecursiveDecrement.java"); + assertAssignments(error, assignment("x", "1"), assignment("#x", "0")); + } + + @Test + void integerDivisionIncludesInputAndGeneratedReturn() { + RefinementError error = verify("ErrorIntegerDivision.java"); + assertAssignments(error, assignment("x", "1"), assignment("#ret", "0")); + } + + @Test + void dependentUpperBoundIncludesBoundaryValuesInBinderOrder() { + RefinementError error = verify("ErrorDependentUpperBound.java"); + assertAssignments(error, assignment("len", "1"), assignment("i", "0"), assignment("#ret", "1")); + } + + @Test + void literalZeroHasNoCounterexampleBecauseValueIsAlreadyKnown() { + RefinementError error = verify("ErrorLiteralZero.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void identityRetainsInputAndReturnSelectedByTheModel() { + RefinementError error = verify("ErrorIdentity.java"); + assertAssignments(error, assignment("x", "0"), assignment("#ret", "0")); + } + + @Test + void staticFinalConstantHasNoCounterexampleBecauseValueIsAlreadyKnown() { + RefinementError error = verify("ErrorStaticFinalConstant.java"); + assertTrue(error.getCounterexample().isEmpty()); + } + + @Test + void knownReturnAssignmentIsRemovedWhileDependentAssignmentsRemain() { + RefinementError error = verify("ErrorDependentRefinement.java"); + assertAssignments(error, assignment("smaller", "0"), assignment("bigger", "21")); + } + + @Test + void multipleParametersAndGeneratedReturnFollowBinderOrder() { + RefinementError error = verify("ErrorFunctionDeclarations.java"); + assertAssignments(error, assignment("d", "0"), assignment("i", "1"), assignment("#ret", "2")); + } + + @Test + void variableUpdateIncludesNegativeInputAndGeneratedReturn() { + RefinementError error = verify("ErrorAssignmentBeforeReturn.java"); + assertAssignments(error, assignment("x", "-1"), assignment("#ret", "0")); + } + + @Test + void pathConditionIsOmittedWhileRecursiveArgumentRemains() { + RefinementError error = verify("ErrorRecursion.java"); + assertAssignments(error, assignment("k", "0"), assignment("#k", "-1")); + } + + @Test + void booleanCounterexampleIncludesInputAndGeneratedReturn() { + RefinementError error = verify("ErrorBoolean.java"); + assertAssignments(error, assignment("value", "false"), assignment("#ret", "false")); + } + + private static RefinementError verify(String test) { + CommandLineLauncher.launch(TEST_SUITE + test); + List errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return assertInstanceOf(RefinementError.class, errors.getFirst()); + } + + @SafeVarargs + private static void assertAssignments(RefinementError error, Pair... expectedAssignments) { + // get counterexample assignments without instance numbers in variable names + List> actualAssignments = error.getCounterexample().assignments().stream() + .map(assignment -> assignment(assignment.first().replaceAll("_[0-9]+$", ""), assignment.second())) + .toList(); + assertEquals(List.of(expectedAssignments), actualAssignments); + } + + private static Pair assignment(String name, String value) { + return new Pair<>(name, value); + } +} From d5aed162a4fd90501639114b6961789501e9d092 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 23 Jul 2026 18:19:19 +0100 Subject: [PATCH 6/6] Remove Unused Imports --- .../java/liquidjava/processor/refinement_checker/VCChecker.java | 1 - .../java/liquidjava/rj_language/opt/VCSimplificationResult.java | 2 -- .../src/main/java/liquidjava/smt/TranslatorToZ3.java | 1 - .../src/test/java/liquidjava/api/tests/TestCounterexamples.java | 2 +- .../src/test/java/liquidjava/api/tests/TestExamples.java | 2 -- 5 files changed, 1 insertion(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index d2ba3cc1..45cb6813 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -23,7 +23,6 @@ import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; -import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index 8fe00a84..05228afc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -2,8 +2,6 @@ import java.util.ArrayList; import java.util.List; -import java.util.Objects; - import liquidjava.processor.VCImplication; /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 981f5a13..8eb366ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -3,7 +3,6 @@ import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.EnumSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 77fb3692..9d45cde0 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -86,7 +86,7 @@ private static RefinementError verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); List errors = Diagnostics.getInstance().getErrors().stream().toList(); assertEquals(1, errors.size(), "Expected exactly one error from " + test); - return assertInstanceOf(RefinementError.class, errors.getFirst()); + return assertInstanceOf(RefinementError.class, errors.get(0)); } @SafeVarargs diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index c2464d70..e739915f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -13,8 +13,6 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; -import liquidjava.diagnostics.errors.*; - import liquidjava.diagnostics.errors.LJError; import liquidjava.utils.Pair;