(declare-fun x () (_ BitVec 8))
(assert (not (= (bvsrem x #xff) #x00)))
(check-sat)
unsat

Doesn't look undefined to me. In general shouldn't we be implementing the
same semantics for our data types that smtlib does? Or at least using a
semantics that we can encode in smtlib? Otherwise our interpreter will be
unsound, right?