Z3PY 방정식, 내가하고 싶은 Z3PY에서 일하고 있어요

Question

크기 제한은

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

내 문제가있는 방정식의 계산의 크기를 제한하는 방법을 알고 그 (CONST * (V0 '의 계산 + const * (func (v0 * const) - v0)) - v0) '가 64 비트보다 큽니다.

Answer 1

Z3의 정수 (일반적으로 SMT 솔버)는 기계 정수 표현으로 한정되지 않습니다. 후드에서는 임의의 크기 정수로 계산할 수있는 큰 정수 표현을 사용합니다.