Hi,
For this formula:
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(assert (bvsle a b))
(check-sat-using qfufbv_ackr)
(get-model)
Z3 gives an invalid model:
(model
(define-fun b () (_ BitVec 2)
#b10)
(define-fun a () (_ BitVec 2)
#b11)
)
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: b68efe4