Z3には次のモデルがあります（コードをhttp://research.microsoft.com/en-us/um/redmond/projects/z3/に貼り付けて試してください）。Webインターフェースは私に解決策を与えてくれます。以下を参照してください。ただし、.NETを介して同じモデルを解き、Evaluate（）を使用して変数値を取得すると、別の出力が得られますが、これは理解できません。ご覧のとおり、値ではなく式を取得します。私の質問は、.NETで値を取得するにはどうすればよいですか？ちなみに、.NETで作成したモデルがここに貼り付けたモデルと同じであることを再確認しました。この投稿も見ました：投稿して修正を適用しようとしました（auto_configをfalseに設定）が、ソルバーがソリューションを計算できなくなるだけです。
モデル：
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インターフェイスソリューション：
[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ソリューション：
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)