How to get concrete values from FuncInterp in Z3 python?

Question

I used the Z3 Solver to check some query and get the model. But some of the variables in the model are FuncInterp, shown as Lambda functions.

[v0 = Lambda(k!0, If(k!0 == 1, 4, 0)),
 v1 = Lambda(k!0,
                  If(k!0 == 1,
                     1,
                     If(k!0 == 3,
                        128,
                        If(k!0 == 2, 113, 0)))),
 v2 = Lambda(k!0, If(k!0 == 1, 1, 0)),
 v3 = Lambda(k!0,
                  If(k!0 == 1,
                     244,
                     If(k!0 == 3,
                        216,
                        If(k!0 == 2, 214, 198)))),
 v4 = Lambda(k!0,
                  If(k!0 == 3,
                     198,
                     If(k!0 == 1,
                        214,
                        If(k!0 == 2, 244, 215)))),
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80)]

Even I tried using z3.set_param('model_compress', False) as suggested in How get a a value from a Lambda expression? They are still like:

[v0 = [0 -> 0, 1 -> 4, else -> 0],
 v1 = [0 -> 0,
       2 -> 113,
       3 -> 128,
       1 -> 1,
       else -> 0],
 v2 = [2 -> 0,
       0 -> 0,
       3 -> 0,
       1 -> 1,
       else -> 0],
 v3 = [0 -> 198,
       2 -> 214,
       3 -> 216,
       1 -> 244,
       else -> 198],
 v4 = [0 -> 215,
       2 -> 244,
       1 -> 214,
       3 -> 198,
       else -> 215],
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80),
 k!7 = [2 -> 0, 0 -> 0, 3 -> 0, 1 -> 1, else -> 0],
 k!4 = [0 -> 0, 1 -> 4, else -> 0],
 k!8 = [0 -> 215, 2 -> 244, 1 -> 214, 3 -> 198, else -> 215],
 k!5 = [0 -> 0, 2 -> 113, 3 -> 128, 1 -> 1, else -> 0],
 k!6 = [0 -> 198, 2 -> 214, 3 -> 216, 1 -> 244, else -> 198]]

My question is, how can I get the constant/concrete values for these FuncInterp?

Many thanks,