(declare-fun n () (_ BitVec 32))
(declare-fun ~ () (_ BitVec 32))
(assert (distinct (_ bv0 32) (bvadd n ~)))
(push 1)
(assert (= (bvadd n (_ bv2 32)) (bvneg (bvadd ~ (bvmul n (_ bv2 32))))))
(push 1)
(assert (= (_ bv0 32) (bvadd n (_ bv1 32))))
(set-info :status unsat)
(check-sat)