Z3PY equation, size limitation

2
votes

I'm working on Z3PY i would like to know how to limit the size of the calculation of a equation

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

my problem is that the calculation of '(const*(v0 + const*(func(v0*const) - v0)) - v0)' is bigger than 64 bits

1
pythonmathz3z3py

1 Answers

1
votes

Integers in Z3 (and generally in SMT solvers) are not bounded by machine integer representations. Under the hood it uses big-integer representations that allow calculating with arbitrary size integers.