The step forward that I believe worked well here is that given some actual paths (and since they are simply a sequence of Instruction, they can be fed to an int

The step forward that I believe worked well here is that given some actual paths (and since they are simply a sequence of Instruction, they can be fed to an interpreter) they are merged or forked while entering or exiting SCCs, this allows to keep a low count of actual visit but exploring a big enough set of path to prove that it covers all possible executions. On the second part, I have to do some thinking and coming back, thanks!