z3 bitvector operation simplified answer

Question

Is there an easier way to get the immediate answers when doing bit-vector ops eg. a = 1 million, b = 0, what is a & b (answer: 0)

This method works but have to introduce dummy variable to store answer:

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(declare-const ans (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(assert (= ans (bvand a b)))
(check-sat)
(get-model)

This method is what I'd like but my code gives a demorgan identity:

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(simplify (bvand a b))

Answer 1

You can use the model to evaluate arbitrary expressions, for instance like this:

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(check-sat)
(eval (bvand a b))

says

sat
#x0000000000000000