java - ジェネリックを使用したOpenJML?

Question

クラスがありEdge.javaます。OpenJML で実行すると、次のようになります。

error: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: com.sun.tools.javac.code.Symbol$TypeSymbol cannot be cast to com.sun.tools.javac.code.Symbol$ClassSymbol

奇妙なことに、私はまだ jml 表記を入れ始めていません。

私のjdkは1.7で、openjmlは最新です（確認のために両方を再ダウンロードしました）。

これは、openjml を実行するために使用されるコマンドです (サイトの例に従います)。 java -jar "E:\Downloads\openjml\openjml.jar" -esc -prover z3_4_3 -exec "E:\Downloads\z3-4.3.0-x64\bin\z3.exe" -noPurityCheck Test.java

編集:ジェネリックを持つ非常に単純なクラスでさえ、このエラーを引き起こす可能性があることを確認できます:

public class Test<T> {
    T i;
}

Edge.java

public class Edge<K> implements Comparable<Edge<K>> {
    public K n1, n2;
    public int weight;

    public final int tiebreaker;
    public static int nextTiebreaker = 0;

    public Edge(K n1, K n2, int weight) {
        this.n1 = n1;
        this.n2 = n2;
        this.weight = weight;
        tiebreaker = nextTiebreaker++;
    }

    @Override
    public int compareTo(Edge<K> o) {
        if(this.weight > o.weight) return +1;
        if(this.weight < o.weight) return -1;

        return tiebreaker - o.tiebreaker; //Same cost, pick one to be the "larger" 
    }
}