Z3PY方程，大小限制

Question

我的工作Z3PY我想知道如何限制一個公式的計算規模

v0 = Int('v0') 
    const = 0x12345678 
    I wrote this : 
s.add((const*(v0 + const*(func(v0*const) - v0)) - v0) == somevalueof64bits) 

我的問題是，「（常量*（V0計算+ const *（func（v0 * const） - v0）） - v0）'大於64位

Answer 1

Z3中的整數（通常在SMT解算器中）不受機器整數表示限制。在它下面它使用大整數表示，允許用任意大小的整數進行計算。