Understanding the bmc-depth bottleneck

[PetarMax]

In real-world proofs that use bmc-depth and are sufficiently large (1000+ nodes), there is a massive slowdown introduced by the associated computations, to the point that a Kontrol proof that passes without bmc-depth in ~1h45m does not finish after more than a day with bmc-depth activated. The manifestation of this, at least on my machine and with 6 parallel threads, is a python process that is constantly at 100% and a kore-rpc-booster process that is way below its maximal throughput. The reasons for this could be:

• the computation of shortest_path when understanding the next steps, which needs to traverse the KCFG and does not appear to rely on dynamic programming and may be forcing thread synchronisation:

  k/pyk/src/pyk/proof/reachability.py

  Line 182 in 76c534f

  shortest_path: list[KCFG.Node] = []

• the computation of same_loop, which extracts and examines cells in a CTerm, which could be costly:

  k/pyk/src/pyk/proof/reachability.py

  Line 793 in 76c534f

  if self.kcfg_explore.kcfg_semantics.same_loop(node.cterm, step.node.cterm):