Crash "Expr cannot be cast to BoolExpr": the type of return in a state refinement leaks into later specs #440

Two external specs, no client code. Checking them crashes:

package a;  // checked first (packages are checked in alphabetical order)

@StateSet({"empty", "maybeElements"})
@ExternalRefinementsFor("java.util.Vector")
public interface VectorSpec<E> {
    @StateRefinement(from = "empty(this)", to = "maybeElements(this)")
    public E set(@Refinement("_ >= 0") int index, E element);
}

package b;

@StateSet({"start", "canEdit"})
@ExternalRefinementsFor("javax.swing.undo.UndoManager")
public interface UndoManagerSpec {
    @StateRefinement(to = "start(this)")
    void UndoManager();

    @StateRefinement(from = "start(this)", to = "!return && start(this)")
    boolean canUndo();
}

Observed (main 1a506fe): Error: class com.microsoft.z3.Expr cannot be cast to class com.microsoft.z3.BoolExpr, pointing at !return && start(this). With int indexOf(Object) in place of set, it says IntExpr cannot be cast to BoolExpr.

Expected: Correct! Passed Verification. Each spec passes on its own, and the pair passes when the packages are in the other order.

Cause. In AuxStateHandler.createStatePredicate, a to of a non-void method is checked by renaming return to _ and declaring _ with the method's return type. That declaration (and the this variables) goes into the current context, outside any scope, and is guarded by !hasVariable(Keys.WILDCARD). So the first non-void method with a to fixes the type of _ for every later spec: here _ : E, and !_ in canUndo is then built on a non-boolean term.

if (returnType != null && !tc.getContext().hasVariable(Keys.WILDCARD))
    tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e);

Possible fix. Wrap the declarations and the SMT check in createStatePredicate in tc.getContext().enterContext() / exitContext() (in a finally), so each method's return has its own type. I tried this locally: the repro above and the int variant both pass, and mvn test on the verifier passes (496 tests, 0 failures).

Where it came up. In a study project with six exercises, a java.util.Vector spec (where set returns E) was checked before an UndoManager spec that uses !return in canUndo/canUndoOrRedo. The UndoManager exercise's real error became this crash. With each exercise in its own project, the error is reported correctly.