Running... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 6417s | 11/50000 samples | 8 samples/sRunning... [                                        ] 0% | ETA: 2692s | 28/50000 samples | 19 samples/sRunning... [                                        ] 0% | ETA: 1890s | 43/50000 samples | 27 samples/sRunning... [                                        ] 0% | ETA: 1365s | 63/50000 samples | 37 samples/sRunning... [                                        ] 0% | ETA: 1197s | 76/50000 samples | 42 samples/sRunning... [                                        ] 0% | ETA: 820s | 117/50000 samples | 61 samples/sRunning... [                                        ] 0% | ETA: 712s | 142/50000 samples | 70 samples/sRunning... [                                        ] 0% | ETA: 693s | 153/50000 samples | 72 samples/sRunning... [                                        ] 0% | ETA: 694s | 160/50000 samples | 72 samples/sRunning... [                                        ] 0% | ETA: 303s | 162/50000 samples | 70 samples/sRunning... [                                        ] 0% | ETA: 337s | 165/50000 samples | 68 samples/sAn example execution:

[State 0]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: true,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 0,
  hubDrop::relay::pending: Set(),
  hubDrop::relay::phase: Init,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set(),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 0,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 1]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
  hubDrop::relay::hLen: 1,
  hubDrop::relay::hPaths: Map(0 -> Set("a", "c"), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: true,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 0,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 2]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
  hubDrop::relay::hLen: 1,
  hubDrop::relay::hPaths: Map(0 -> Set("a", "c"), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: true,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 1,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 3]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set("a"),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(
      0 -> Set(3),
      1 -> Set(),
      2 -> Set(),
      3 -> Set(),
      4 -> Set(),
      5 -> Set()
    ),
  hubDrop::relay::qLen: 1,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 1,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 4]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set("a"),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(
      0 -> Set(3),
      1 -> Set(),
      2 -> Set(),
      3 -> Set(),
      4 -> Set(),
      5 -> Set()
    ),
  hubDrop::relay::qLen: 1,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 1,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 5]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set("a"),
  hubDrop::relay::hubSent: Set("b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(3), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Other, 1 -> Chunks, 2 -> Eof),
  hubDrop::relay::wLen: 3,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 6]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("a", "b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(3), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Other, 1 -> Chunks, 2 -> Eof),
  hubDrop::relay::wLen: 3,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 7]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("a", "b", "c"),
  hubDrop::relay::imported: Set(),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a", "c"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(),
  hubDrop::relay::wChunks: Map(0 -> Set(3), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Chunks, 1 -> Eof, 2 -> Nil),
  hubDrop::relay::wLen: 2,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 8]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("a", "b", "c"),
  hubDrop::relay::imported: Set("c"),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 1,
  hubDrop::relay::pending: Set("a"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(3),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Eof, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 1,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 9]
{
  hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::hLen: 0,
  hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubDrop::relay::have: Set("b"),
  hubDrop::relay::hubComputing: Set(),
  hubDrop::relay::hubErr: false,
  hubDrop::relay::hubFirstNeed: false,
  hubDrop::relay::hubOutbox: Set(),
  hubDrop::relay::hubSent: Set("a", "b", "c"),
  hubDrop::relay::imported: Set("c"),
  hubDrop::relay::inline: Set("b", "c"),
  hubDrop::relay::outstanding: 0,
  hubDrop::relay::pending: Set("a"),
  hubDrop::relay::phase: Staging,
  hubDrop::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubDrop::relay::qLen: 0,
  hubDrop::relay::recipes: Set("c"),
  hubDrop::relay::rounds: 0,
  hubDrop::relay::store: Set(3),
  hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubDrop::relay::wLen: 0,
  hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[violation] Found an issue (2581ms at 64 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0xe7b193ae3b3c5b4e --backend=rust to reproduce.
error: Invariant violated