为什么Z3将极小实数舍入为1.0/0.0？如何用Python浮点数正常运行？

Z3的Real类型底层是精确有理数实现，本身不直接支持浮点数运算。当你传入Python原生float类型的数值参与Real类型运算时，Z3会自动执行「浮点数转精确有理数」的转换逻辑。
0.00001这类很小的十进制小数本身无法被二进制浮点数精确表示，Z3的转换逻辑在处理这类极小（或者极大）的浮点数值时，会出现计算溢出，导致生成分母为0的非法有理数，也就是你在smt2输出里看到的/ 1.0 0.0，本质是构造了无穷大值，后续C++底层运算时直接触发除以零的浮点异常。
而你直接用Q(1,100000)构造有理数的方式，跳过了浮点数转有理数的步骤，生成的是合法的精确分数，所以不会触发问题。

• 做数值缩放预处理：如果你的约束里所有浮点系数的量级一致，可以统一把约束两边乘以10的N次方，把小系数放大为整数，比如你案例里的约束可以等价改写为 a + b > 0，完全规避小系数转换问题，这种方法性能损耗最低。
• 封装浮点数转有理数的转换逻辑：借助Python标准库fractions.Fraction做精确转换，再映射为Z3的有理数，适合系数量级差异大、无法统一缩放的场景，示例工具函数如下：

from fractions import Fraction
def float_to_z3_real(f):
    num, den = Fraction(f).as_integer_ratio()
    return Q(num, den)

使用时把你的浮点系数用这个函数包裹即可：s.add(float_to_z3_real(0.00001) * Real("a") + float_to_z3_real(0.00001) * Real("b") > 0.0)

• 切换为浮点排序：如果你的业务场景不需要严格的精确实数运算，可直接使用Z3的浮点类型Float64替代Real，原生适配Python浮点数运算，不会触发转换异常。

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