Search code examples
z3

Is there a maximum value size for variables?

Suppose I have the following (intentionally simple) subsection of constraints:

..... SOME STUFF .....

(declare-const I Int)
(assert (and (>= I 0) (<= I 1)))

(define-fun W () Int
    2251799813685248
)

..... MORE STUFF .....

(maximize (* I W))
(check-sat)
(get-model)

Is the size I'm giving to W too big? Or more generally, is there a maximum size value that can be assigned in Z3 (for example if variables are stored as regular ints/floats/longs/etc instead of with variable precision)?

Solution

  • An Int value corresponds to a mathematical integer. It can be of an arbitrary size. There are no maximums.

    For sized versions, you should use bit-vectors: (_ BV n) is the type of a bit-vector of size n, which follows machine arithmetic rules.