I can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult

I can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers. If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.