Reusing Ghost variable names for classes in the same folder generates an error
Example
Currently the following example gives an error:
@ExternalRefinementsFor("java.util.ArrayDeque")
@Ghost("int size")
public interface ArrayDequeRefinements<E> {
}
@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ListRefinements<E> {
@StateRefinement(to = "size(this) == 0")
void f(); // <-- error here
}
The error provided is Sort mismatch at argument #1 for function (declare-fun size (java.util.ArrayDeque) Int) supplied sort is java.util.ArrayList
This error shows up on the function coupled to the first Refinement that references the variable and not on the variable declaration
Intended behavior
Allow different classes to have the same Ghost variable names and disambiguate between them