Z3 使用 bitVecs 获得无溢出的解决方案

Question

我发现这篇文章提供了一种在添加 bitVecs 时检查解决方案溢出的方法 z3 bitvector 从 python 溢出检查？

但是，它仅在仅添加 2 个 bitVec 时才有效，是否有任何方法可以扩展它以便添加任意数量的 bitVec？ 据我所知，问题是“z3._coerce_exprs(x, y)”在

def bvadd_no_overflow(x, y, signed=False):
    assert x.ctx_ref()==y.ctx_ref()
    a, b = z3._coerce_exprs(x, y)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), 
         b.as_ast(), signed))

只能接受2个输入。