Skip to content

Commit 1d7b0c6

Browse files
committed
Add Variable Instance Regardless of Matching State
This is because we want to show the failed variable instance in the context debugger and otherwise it is never added to the context. Not sure if this change is correct.
1 parent 4f0272b commit 1d7b0c6

1 file changed

Lines changed: 3 additions & 2 deletions

File tree

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

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -482,7 +482,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
482482
expectState = expectState.changeOldMentions(vi.getName(), instanceName);
483483

484484
found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
485-
if (found && stateChange.hasTo()) {
485+
if (stateChange.hasTo()) {
486486
String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
487487
Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)
488488
.substituteVariable(Keys.THIS, newInstanceName);
@@ -492,7 +492,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
492492
transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName);
493493
// update of state of new instance of this#n#(whatever it was + 1)
494494
addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation);
495-
return;
495+
if (found)
496+
return;
496497
}
497498
}
498499
if (!found) { // Reaches the end of stateChange no matching states

0 commit comments

Comments
 (0)