Skip to content

Commit 055e933

Browse files
fix bug gathering predicates
1 parent 8805dab commit 055e933

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

  • liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -389,6 +389,7 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun
389389
String customMessage) throws StateRefinementError {
390390
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
391391
gatherVariables(found, lrv, mainVars);
392+
gatherVariables(expected, lrv, mainVars);
392393
TranslationTable map = new TranslationTable();
393394
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
394395
throw new StateRefinementError(position, expected.simplify(context),

0 commit comments

Comments
 (0)