Does Z3 use bounds on Bitvectors to reduce them to lower size/width?

[ThomasHaas]

I have a bounded model checking application which encodes the data-flow of a program with 64-bit bitvectors.
Using static analysis, it may be possible to derive a priori bounds on bv-variables, that would allow them to be encoded with less bits.
Say I know that some variable is bounded by 2^16, I'm wondering if there is a difference in directly encoding the variable as 16-bit or as 64-bit but asserting 0 <= V <= 2^16 as an additional constraint.
Will this constraint be used to effectively reduce the variable down to 16 bit during Bit-blasting and then get discarded entirely?

I'm asking this for two reasons:

• First, it would be a lot easier to keep the variables as 64-bit in the encoding and just let Z3 decide how many bits it actually needs.
• Second, I noticed performance degradations when adding such interval constraints on an integer-based encoding, i.e., adding variable bounds in LIA can make matters worse (by multiple factors in my use-case). However, I suspect that in the case of bitvectors, the constraints are used only for the bit-blasting and then effectively thrown away, so that there is no way that I get performance degradation by adding interval information.

As a side question: Does Z3 try to infer bounds automatically to reduce the Bit-Blasting? If so, is it possible to check how many boolean variables it actually ended up creating to get a gist of how well it derived bounds? In particular, It would be interesting to see if adding explicit bounds to some variables actually reduces the bit-blasted formula (if not, then Z3 was able to derive the bounds by itself).

[NikolajBjorner]

It tries to, but in the current tactic called reduce-bv-size it doesn't detect this pattern.
Since we are close to a release, I am adding a pass that is currently disabled to detect unsigned upper bounds.
It is also very restrictive but covers a basic use case, such as

(declare-const x (_ BitVec 64))
(assert (bvule x (_ bv256 64)))
(assert (= (bvmul x x) x))
(check-sat)

Bit-size reduction would only be available as pre-processing so your BMC queries cannot use the incremental mode.

[ThomasHaas]

I understand the problem with incrementality if I add such bounds later on.
But can't Z3 use full optimiziations on all the formulas asserted before the first push?
In my case, I would add the bounds initially and only add other types of constraints incrementally.

[NikolajBjorner]

You can try it out smt.bv.size_reduce=true