小编Yan*_*Yan的帖子

我正在尝试将 z3py 集成到我的应用程序中。有涉及小实数的断言，例如

solver.add(x <= 1e-6)

然后我收到以下错误：

File "~/src/solver/z3.py", line 2001, in __le__
  a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
  b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
  return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
  raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'

虽然断言

solver.add(x <= 1e-4)

似乎没问题。

因此，我猜测 z3 中存在某种精度限制。如果是这样，是否可以选择让第一个断言通过？

谢谢。