Say you have a BitVector of 64 bits and want to express the replacement of bits 8 to 15 with some other value. Which would be the most efficient way to do so?
The best way would be to extract the top and bottom parts, and splice the replacement directly inside. Like this:
(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun original () (_ BitVec 64))
(declare-fun replacement () (_ BitVec 8))
(define-fun result () (_ BitVec 64) (concat ((_ extract 63 16) original)
replacement
((_ extract 7 0) original)))
(assert (= (bvadd original #x0000000000000100) result))
(check-sat)
(get-value (original replacement result))
This prints:
sat
((original #x0000000000000000)
(replacement #x01)
(result #x0000000000000100))
Note that the alternative way of shifting and masking can work as well, though in my experience avoiding arithmetic is the way to go if you can do so. (That is, and-mask with the 0-bytes in the correct place, shift your replacement to left and do a bit-wise or.) But as with any question that asks "best way," the answer is to try different options and benchmark them. Different encodings might perform better with different problems.