[571] % z3-4.8.7 small.smt2
sat
sat
[572] % z3-4.8.8 small.smt2
unsat
sat
[573] % z3release small.smt2
unsat
sat
[574] % 
[574] % cat small.smt2
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(assert (= (bvnand a b) a))
(check-sat-using (then simplify reduce-invertible smt))
(check-sat)
[575] %