Unsoundness in elim-uncnstr2

[nunoplopes]

(declare-fun undef!34 () (_ BitVec 32))
(declare-fun |np_%y#2| () Bool)
(declare-fun undef!35 () (_ BitVec 32))
(declare-fun undef!39 () (_ BitVec 32))
(declare-fun |%y#3| () (_ BitVec 32))
(declare-fun |isundef_%y#3| () (_ BitVec 1))
(declare-fun |%y#1| () (_ BitVec 32))
(declare-fun |%y#2| () (_ BitVec 32))
(declare-fun |%x#0| () (_ BitVec 32))

(assert (forall ((undef!4 (_ BitVec 32))
                     (undef!9 (_ BitVec 32))
                     (undef!14 (_ BitVec 32))
                     (undef!19 (_ BitVec 32))
                     (undef!31 (_ BitVec 32)))
              (let ((a!1 (or |np_%y#2|
                                (not (bvsle |%y#1| undef!9))
                                (not (bvsle undef!4 |%x#0|))))
                       (a!3 (not (bvsle (ite (= |isundef_%y#3| #b0) |%y#3| undef!31)
                                        undef!19)))
                       (a!5 (ite (bvsle (ite (= |isundef_%y#3| #b0) |%y#3| undef!39)
                                        undef!35)
                                 #b0
                                 #b1))
                       (a!6 (ite (bvsle |%y#2| undef!34) #b0 #b1)))
                 (let ((a!4 (ite (or a!3 (not (bvsle |%y#2| undef!14))) #b1 #b0)))
                   (not (or (not a!1) (= a!4 (bvor a!5 a!6))))))))

(check-sat-using (then elim-uncnstr2 smt))
(check-sat)

prints:

sat
unsat