Skip to content

Commit ea87100

Browse files
committed
Fix
1 parent 2270950 commit ea87100

File tree

3 files changed

+5
-6
lines changed

3 files changed

+5
-6
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ public String getDetails() {
3535
.reduce((a, b) -> a + " && " + b).orElse("");
3636

3737
// check if counterexample is trivial (same as the found value)
38-
if (counterexampleExp.equals(found.getValue().toSimplifiedString()))
38+
if (counterexampleExp.equals(found.getValue().toString()))
3939
return "";
4040
return "Counterexample: " + counterexampleExp;
4141
}

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -146,9 +146,9 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJEr
146146
}
147147

148148
/**
149-
* Gets function declarations when an exact qualified name lookup fails. Tries to match by simple
150-
* name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise
151-
* returns the first compatible candidate and relies on later coercion via var supertypes.
149+
* Gets function declarations when an exact qualified name lookup fails. Tries to match by simple name and number of
150+
* parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first
151+
* compatible candidate and relies on later coercion via var supertypes.
152152
*/
153153
private FuncDecl<?> resolveFunctionDecl(String name, Expr<?>[] params) throws LJError {
154154
String simple = Utils.getSimpleName(name);

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
5050

5151
private static boolean hasRefinementValue(CtAnnotation<?> annotation, String refinement) {
5252
Map<String, ?> values = annotation.getValues();
53-
return Stream.of("value", "to", "from")
54-
.anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
53+
return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
5554
}
5655
}

0 commit comments

Comments
 (0)