équation Z3PY, la taille limite

Question

Je travaille sur Z3PY je voudrais savoir comment limiter la taille du calcul d'une équation

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

mon problème est que le calcul de « (const * (v0 + const * (func (v0 * const) - v0)) - v0) 'est supérieur à 64 bits

Answer 1

Les entiers dans Z3 (et généralement dans les solveurs SMT) ne sont pas délimités par des représentations d'entier machine. Sous le capot, il utilise des représentations de grands nombres entiers qui permettent de calculer avec des entiers de taille arbitraire.