(set-logic QF_BV)
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(assert (distinct 
 (bvurem a b) #b0))
(assert (distinct b #b0))
(check-sat)
(exit)