Termination plugin fails with unclear error

[Aurel300]

The following snippet verifies, but does not prove termination:

generic_search.vpr

domain T {}

adt Ordering {
    Less()
    Equal()
    Greater()
}

domain PartialCmp[DomT] {
    function compare(self: DomT, other: DomT): Ordering
    axiom { forall a: DomT, b: DomT :: {compare(a, b)} (compare(a, b) == Equal()) == (a == b) }
    axiom { forall a: DomT, b: DomT, c: DomT :: {compare(a, b), compare(b, c)} compare(a, b).isLess && compare(b, c).isLess ==> compare(a, c).isLess }
}

method binary_search(data: Seq[T], key: T)
    returns (found: Bool)
    requires forall a: Int, b: Int :: {data[a], data[b]} 0 <= a < b < |data| ==> !compare(data[a], data[b]).isGreater
    ensures found == (key in data)
    //decreases
{
    var lo: Int := 0
    var hi: Int := |data|
    found := false
    while (!found && lo < hi)
        invariant 0 <= lo <= hi <= |data|
        invariant !found ==> !(key in data[..lo]) && !(key in data[hi..])
        invariant found ==> (key in data)
        //decreases hi - lo
    {
        var mid: Int := lo + (hi - lo) / 2
        if (compare(data[mid], key).isLess) {
            lo := mid + 1
        } elseif (compare(data[mid], key).isEqual) {
            found := true
        } else {
            hi := mid
        }
    }
}

When the loop variant decreases hi - lo is added, the IDE reports errors with no positions, i.e., the status bar says "4 errors due to imported files":

• Constructing the AST has failed: Consistency error: Domain function decreasing with formal arguments List(arg1: T, arg2: T) cannot be applied to provided arguments List(int1, int2). (int.vpr@9.41--9.63)
• Constructing the AST has failed: Consistency error: Domain function decreasing with formal arguments List(arg1: T, arg2: T) cannot be applied to provided arguments List(int1, int2). (int.vpr@10.31--10.53)
• Constructing the AST has failed: Consistency error: Domain function bounded with formal arguments List(arg1: T) cannot be applied to provided arguments List(int1). (int.vpr@13.30--13.43)
• Constructing the AST has failed: Consistency error: Domain function bounded with formal arguments List(arg1: T) cannot be applied to provided arguments List(int1). (int.vpr@14.27--14.40)

Why is it failing this way? The termination measure is just an integer -- does the termination plugin try to use the "generic" type in constructing the proof here?

Note that the monomorphic/integer version verifies fine, including the termination measures (as expected).

monomorphic_search.vpr

method binary_search(data: Seq[Int], key: Int)
    returns (found: Bool)
    requires forall a: Int, b: Int :: {data[a], data[b]} 0 <= a < b < |data| ==> data[a] <= data[b]
    ensures found == (key in data)
    decreases
{
    var lo: Int := 0
    var hi: Int := |data|
    found := false
    while (!found && lo < hi)
        invariant 0 <= lo <= hi <= |data|
        invariant !found ==> !(key in data[..lo]) && !(key in data[hi..])
        invariant found ==> (key in data)
        decreases hi - lo
    {
        var mid: Int := lo + (hi - lo) / 2
        if (data[mid] < key) {
            lo := mid + 1
        } elseif (data[mid] == key) {
            found := true
        } else {
            hi := mid
        }
    }
}

[marcoeilers]

The problem is that the domain name T clashes with the type parameter T of the WellFoundedOrder domain that's implicitly imported by the termination plugin.
I'll think about how to fix it.