Search code examples
z3

Checking Overflow of `bvmul` in Z3

I'd like to run the following query, which checks if multipling two bitvectors with bvmul and saturating the result as the max/min value is monotonic, i.e. if a <= b, then (bvmul_saturated a c) <= (bvmul_saturated b c):

(declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))
(declare-const amc (_ BitVec 32))
(declare-const bmc (_ BitVec 32))
(declare-const asat (_ BitVec 16))
(declare-const bsat (_ BitVec 16))
(assert (bvule a b))
(assert (= amc (bvmul (concat #x0000 a) (concat #x0000 c))))
(assert (= bmc (bvmul (concat #x0000 b) (concat #x0000 c))))
(assert (= asat (ite (bvugt ((_ extract 31 16) amc) #x0000) #xffff ((_ extract 15 0) amc))))
(assert (= bsat (ite (bvugt ((_ extract 31 16) bmc) #x0000) #xffff ((_ extract 15 0) bmc))))
(assert (not (bvule asat bsat)))
(check-sat)

However, even with long timeouts (10+ minutes), Z3 is not able to prove the above formula is unsat, and instead timeouts and returns unknown. Is there a better way to encode this problem, or some Z3 options that will allow the solver to actually solve this problem?

Solution

  • You can use the internal overflow checking predicate:

    bvumul_noovfl -- true if the multiplication of the arguments does NOT overflow

    So, you'd code your problem as:

    (declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))

(assert (bvumul_noovfl a c))
(assert (bvumul_noovfl b c))
(assert (bvule a b))
(assert (not (bvule (bvmul a c) (bvmul b c))))
(check-sat)

    This runs in about 1-minute on my four-year old Mac:

    $ time z3 a.smt2
unsat
z3 a.smt2  65.52s user 0.60s system 99% cpu 1:06.42 total

    Note that checking overflow of multiplication is an expensive operation, so don't expect this to scale up linearly with the bit-size.