You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Using the Dafny IDE 4.3.1 with Dafny 4.8.1, the "Show counterexample (F7)" feature gives an error:
Counterexample request failed: TypeError: Cannot convert undefined or null to object
Repro
Load the following code into VS Code. Notice that an error is reported. Select "Show counterexample" from the right-click Dafny menu or press F7. That gives the error.
method BinarySearch(a: array<int>, key: int) returns (r: int)
requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
ensures 0 <= r ==> r < a.Length && a[r] == key
ensures r < 0 ==> key !in a[..]
{
var lo, hi := 0, a.Length;
while lo < hi
invariant 0 <= lo <= hi <= a.Length
invariant key !in a[..lo] && key !in a[hi..]
{
var mid := lo + (hi - lo) / 2;
if a[mid] == key {
return mid;
} else if key < a[mid] {
hi := mid;
} else {
lo := mid; // there's an error on this line
}
}
r := -1;
}
The text was updated successfully, but these errors were encountered:
Using the Dafny IDE 4.3.1 with Dafny 4.8.1, the "Show counterexample (F7)" feature gives an error:
Repro
Load the following code into VS Code. Notice that an error is reported. Select "Show counterexample" from the right-click Dafny menu or press F7. That gives the error.
The text was updated successfully, but these errors were encountered: