ビットベクトル演算を使用して算術方程式を解くために Z3 を使用しようとしています。実数も扱う方法はないかと思っていました。たとえば、#x1 とは異なる定数を指定して、代わりに実数を使用できるとします。
(set-option :pp.bv-literals false)
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
(assert (= (bvadd x y) #x1))
(check-sat)
(get-model)