Dafny for VSCode times out as "idle" instead of failing verification

[acioc]

Per request from @RustanLeino, I am creating this issue in this repo.

The dafny-lang/dafny repo received the following issue: dafny-lang/dafny#415

Upon investigation, it appears the submitted code times out on the command line but goes from "Verifying" to "Idle" in VSCode without noting the timeout/failure.

Please see the linked issue for more information/ discussion.

The original request was as follows:

We are two students who are using Dafny for the first time and was trying to prove union-find when we ran into weird behavior. Dafny verified some very odd asserts and we could even assert false. We removed as much as possible from the code, but we can in this program, ensure false in main without any requires or assume. We wouldn't think this could happen no matter what code we wrote outside of main but couldn't find any errors either.

class Main {
  method main()
  ensures false;
  {
    var n := new Node;
    n.parent := 0;
    n.lengthToRoot := 0;
    n.root := 0;
    var G := new Node[1](_ => n);
    unite(G, 0, 0);
  }

  predicate graph(G: array<Node>)
    reads G, set i: nat | i < G.Length :: G[i]
  { (forall i: nat :: i < G.Length ==> (
      (G[i].parent < G.Length) &&
      (G[i].lengthToRoot == 0 <==> G[i].parent == i) &&
      (G[i].lengthToRoot > 0 ==> G[G[i].parent].lengthToRoot < G[i].lengthToRoot) &&
      (G[i].lengthToRoot == 0 <==> G[i].root == i) &&
      (G[i].root == G[G[i].parent].root)
    )) &&
    forall i: nat, j: nat :: i < j < G.Length ==> G[i] != G[j]
  }

  method Find(G: array<Node>, a: nat) returns (res: nat)
    requires a < G.Length
    requires graph(G)
    ensures graph(G)

    modifies G, set i: nat | i < G.Length :: G[i]
    decreases G[a].lengthToRoot

    ensures res == G[a].root

    ensures res < G.Length
    ensures G[res].lengthToRoot == 0
    ensures G[res].parent == res
    ensures forall i: nat :: i < G.Length ==> old(G[i].lengthToRoot) == G[i].lengthToRoot
    ensures forall i: nat :: i < G.Length ==> old(G[i]) == G[i]
    ensures forall i: nat :: i < G.Length ==> old(G[i].root) == G[i].root
  {
    if G[a].parent != a {
      G[a].parent := Find(G, G[a].parent);
    }
    return G[a].parent;
  }

  method unite(G: array<Node>, a: nat, b: nat) 
    requires a < G.Length
    requires b < G.Length
    requires graph(G)
    ensures G[a].root == G[b].root;
    ensures G[a].root != G[b].root;
    modifies G, set i: nat | i < G.Length :: G[i]
  {
    var rootA := Find(G, a);
    var rootB := Find(G, b);
  }
}

class Node {
  var parent: nat;
  ghost var lengthToRoot: nat;
  ghost var root: nat;
}

And investigation from @robin-aws showed:

I was able to produce the spurious verification in VSCode. The toolbar at the bottom goes from "Verifying" to "Idle" on this file, taking about 10-15 seconds, and only gives a couple of undecipherable warnings (copy and pasted below):

{
	"resource": "/Users/salkeldr/Documents/GitHub/dafny/Test/git-issues/git-issue-415.dfy",
	"owner": "_generated_diagnostic_collection_name_#0",
	"severity": 2,
	"message": "For expression \"(i < G.Length ==> G[i].parent < G.Length) && (i < G.Length ==> (G[i].lengthToRoot == 0 <==> G[i].parent == i)) && (i < G.Length ==> (G[i].lengthToRoot == 0 <==> G[i].root == i))\":",
	"source": "Dafny VSCode",
	"startLineNumber": 15,
	"startColumn": 5,
	"endLineNumber": 15,
	"endColumn": 1.7976931348623157e+308
}

{
	"resource": "/Users/salkeldr/Documents/GitHub/dafny/Test/git-issues/git-issue-415.dfy",
	"owner": "_generated_diagnostic_collection_name_#0",
	"severity": 2,
	"message": "For expression \"(i < G.Length ==> G[i].lengthToRoot > 0 ==> G[G[i].parent].lengthToRoot < G[i].lengthToRoot) && (i < G.Length ==> G[i].root == G[G[i].parent].root)\":",
	"source": "Dafny VSCode",
	"startLineNumber": 15,
	"startColumn": 5,
	"endLineNumber": 15,
	"endColumn": 1.7976931348623157e+308
}