macOS环境Python z3-solver求解实数约束返回错误结果求助

你遇到的是z3-solver 4.8.12.0版本macOS Python绑定的已知数值解析bug，你的代码本身没有操作错误。
该版本在将Python侧的极小十进制浮点数转换为Z3的Real类型时，数值解析逻辑出错：你传入的0.00001会被错误转换为1/0的非法表达式，该表达式在Z3的算术处理中会被识别为正无穷，因此x=正无穷，y=0.1满足x+y>1的约束，最终求解器返回错误的sat结果。
你在Ubuntu上使用的4.8.10.0版本不存在该解析bug，因此运行结果正确。

• 方案1：降级z3-solver到无bug的版本，执行命令：
  pip install z3-solver==4.8.10.0
• 方案2：规避浮点解析逻辑，直接用字符串或分数形式定义实数值：
  将代码中的x==0.00001替换为x == RealVal("0.00001")或者x == Q(1, 100000)即可，该写法兼容所有z3版本，不会出现解析错误。

内容的提问来源于stack exchange，提问作者Younger