Strange variable values in Z3 solution

Question

I have the following model in Z3 (paste code at http://research.microsoft.com/en-us/um/redmond/projects/z3/ to try it). The web interface gives me a solution back, see below. However, when I solve the same model via .NET and get the variable values by using Evaluate(), I get a different output, which I don't understand. As you can see, I don't get values, but expressions. My question is: How do I get the values in .NET? For the record, I double checked that the model I build up in .NET is identical to the one pasted here. I also saw this post: Post and tried to apply the fix (setting auto_config to false), but that only results in the solver not being able to compute a solution.

Model:

    Q311, Q411, Q431, QQ311, QQ411, QQ431, H11, H41 = Reals('Q311 Q411 Q431 QQ311 QQ411 QQ431 H11 H41')
solve(
Q411 + Q311 <= 155,
Q431 - Q311 <= -28.015,
-Q431 - Q411 <= -126.985,
-Q411 - Q311 <= -155,
-Q431 + Q311 <= 28.015,
Q431 + Q411 <= 126.985,
43.015 - H11 - 0.0031 * QQ311 * Q311 <= 0,
H41 - H11 - 0.0031 * QQ411 * Q411 <= 0,
H41 - 43.015 - 0.0031 * QQ431 * Q431 <= 0,
-43.015 + H11 + 0.0031 * QQ311 * Q311 <= 0,
-H41 + H11 + 0.0031 * QQ411 * Q411 <= 0,
-H41 + 43.015 + 0.0031 * QQ431 * Q431 <= 0,
QQ311 - Q311 <= 0,
QQ411 - Q411 <= 0,
QQ431 - Q431 <= 0,
-QQ311 + Q311 <= 0,
-QQ411 + Q411 <= 0,
-QQ431 + Q431 <= 0,
Q311 >= 0,
Q411 >= 0,
Q431 >= 0,
QQ311 >= 0,
QQ411 >= 0,
QQ431 >= 0,
H11 >= 0,
H41 >= 0,
show=True)

Web interface solution:

[Q411 = 83.5779688745?,
Q311 = 71.4220311254?,
Q431 = 43.4070311254?,
H11 = 27.2015697567?,
QQ311 = 71.4220311254?,
H41 = 48.8559280884?,
QQ411 = 83.5779688745?,
QQ431 = 43.4070311254?]

.NET solution:

Q311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
Q411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)
Q431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
QQ431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
H11: (root-obj (+ (* 160000000000000000 (^ x 2)) (* 41281815903200000000 x) (- 1
241318258533436869359)) 2)
QQ311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
H41: (root-obj (+ (* 40000000000 (^ x 2)) (* (- 19162006800000) x) 8407015578762
89) 1)
QQ411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)

Answer 1

I was able to understand the output after reading this post.

I added { "PP_DECIMAL", "true"} to my context's configuration and now I get decimal values as I expected.