Ah—makes sense. I wonder if attempts at going in the other direction have been made, and initially constraining the structures of the known parts so that you could do something like a subtraction to get the unknown (probably a crazy dead-end idea I realize :).
> But, the "damage" done by `K` is encoded in the state at the interface to `D` and `D` better undo that state to get to identity, which is what the solver would exploit.
Interesting. So because we know it's an inversion scenario beforehand we can modify the solver to not be so general, and only bother considering solutions which modify the state in an inverse manner to our original program...
Cool. I'll be keeping this at the back of my mind to see if any ideas come up. Thanks and good luck!