#StackBounty: #python #z3 How to get concrete values from FuncInterp in Z3 python?

Bounty: 50

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,

Get this bounty!!!

This site uses Akismet to reduce spam. Learn how your comment data is processed.