First trials with SymbolicDict datatype.
TODO: solve that the Z3 model does not include the Array (but it seems that it is included in the input of Z3)