Dafny crash in Translator.FuelSetting.GetFunctionFuel

[jaylorch]

Dafny crashes in Translator.FuelSetting.GetFunctionFuel when verifying the code below:

datatype T = T(n:int)

function ToInt(t:T) : int
    ensures ToInt(t) == int(t.n);
{
    int(t.n)
}

method Test()
{
    assert exists p:int :: exists t:T :: ToInt(t) > 0;
}

[qunyanm]

Fixed

[cpitclaudel]

Neat :) First fixed issue on Github 👍 🎉 ! Btw @qunyanm, a neat feature of github is that if you write "Fixes #1" or "Closes #1" in the commit message, it automatically closes the corresponding ticket with a link to the commit (see cpitclaudel/company-coq#124 for an example)

[qunyanm]

Oh, I didn't know the feature. It will be handy. Thanks for letting me know.