When I send Z3 the trivial:
(declare-fun M (Int) Int)
(check-sat)
(get-value (M))
Z3 answers:
((M (_ as-array M)))
How shall I interpret this answer?
There's a nice isomorphism between functions and arrays in SMTLib. Since arrays are indexed by types, an array indexed by type A to produce type B is essentially a function from A to B.
Z3 takes advantage of this correspondence and allows you to mix/match arrays and functions in this way. So, in your example, it's telling you that M can be any array, (or, any function). The array has no constraints on it, as indicated by (_ as-array M): The way to read this is that all we know is that it's an array (or function by the above isomorphism), but otherwise there are no other constraints on it.
Let's add:
(assert (= (M 12) 13))
Now, z3 says:
((M ((as const (Array Int Int)) 13)))
This one is special syntax for the "constant" array. i.e., an array that stores 13 at each index. Again, you can see this can be interpreted as a function that always returns 13 no matter what the input is.
Let's also add:
(assert (= (M 42) 7))
Now we get:
((M (store ((as const (Array Int Int)) 13) 42 7)))
The way to read is as follows. The "inner" part is the same as before:
(as const (Array Int Int)) 13)
i.e., an array where 13 is stored in every cell. But then we do a store on it:
(store OLD_ARRAY 42 7)
this means we create a new array, where at index 42 we store 7, but otherwise we behave as OLD_ARRAY. Now you can see how z3 can "chain" of new equations on top of old arrays to create new ones.
So, long story short, z3 "conflates" arrays and functions when printing models. While this can be confusing at first, it simply follows the isomorphism between them.
In general, arrays and lambda-functions are isomorphic. There's a short segment in the z3 manual that explains this in some further detail: https://microsoft.github.io/z3guide/docs/logic/Lambdas/#lambdas-as-arrays, which allows use of arrays to simulate some higher-order features.