Skip to content

Commit cb9a1b5

Browse files
committed
Extract getCounterexampleString from getDetails
1 parent 5e003b7 commit cb9a1b5

1 file changed

Lines changed: 9 additions & 0 deletions

File tree

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,10 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
2727

2828
@Override
2929
public String getDetails() {
30+
return getCounterexampleString();
31+
}
32+
33+
private String getCounterexampleString() {
3034
if (counterexample == null || counterexample.assignments().isEmpty())
3135
return "";
3236

@@ -37,9 +41,14 @@ public String getDetails() {
3741
// check if counterexample is trivial (same as the found value)
3842
if (counterexampleExp.equals(found.getValue().toString()))
3943
return "";
44+
4045
return "Counterexample: " + counterexampleExp;
4146
}
4247

48+
public Counterexample getCounterexample() {
49+
return counterexample;
50+
}
51+
4352
public ValDerivationNode getExpected() {
4453
return expected;
4554
}

0 commit comments

Comments
 (0)