Does Z3 have the ability to do power mod arithmetic? For instance, if I'm placing in expressions of the sort x ** y % z, is there a way to tell Z3 that it is this type of expression, similar to how python has the function pow(x,y,z)? My assumption is that would open up solving options (such as modular inverse).
Interesting point. There isn't any particular support for this in Z3. What are the known techniques in this area?
Z3 Power Modulo Statements