(set-logic QF_BV)
(declare-fun v1 () (_ BitVec 2))
(declare-fun v2 () (_ BitVec 2))
(define-fun $e3 () (_ BitVec 2) (_ bv0 2))
(define-fun $e4 () (_ BitVec 2) (bvmul v1 v2))
(define-fun $e5 () (_ BitVec 1) (ite (= $e4 (bvnot $e3)) #b1 #b0))
(assert (not (= (bvnot $e5) #b0)))
(check-sat)
(exit)