Soundness bug in QF_BV with dom-simplify tactic

[numairmansur]

Hi,
On the following satisfiable file, I get unsat when using (check-sat-using dom-simplify)

(set-logic QF_BV)
(assert
 (let (($x16 (or (and (not (= ((_ extract 0 0) (_ bv1 3)) (_ bv1 1))) (= ((_ extract 0 0) (_ bv7 3)) (_ bv1 1))) (and (= ((_ extract 0 0) (_ bv1 3)) (_ bv1 1)) (not (= ((_ extract 0 0) (_ bv7 3)) (_ bv1 1)))))))
 (let (($x21 (or (and (= ((_ extract 0 0) (_ bv1 3)) (_ bv1 1)) (= ((_ extract 0 0) (_ bv7 3)) (_ bv1 1))) (and $x16 (= (_ bv0 1) (_ bv1 1))))))
 (let (($x23 (= (ite $x21 (_ bv1 1) (_ bv0 1)) (_ bv1 1))))
 (let (($x32 (or (and (not (= ((_ extract 1 1) (_ bv1 3)) (_ bv1 1))) (= ((_ extract 1 1) (_ bv7 3)) (_ bv1 1))) (and (= ((_ extract 1 1) (_ bv1 3)) (_ bv1 1)) (not (= ((_ extract 1 1) (_ bv7 3)) (_ bv1 1)))))))
 (let (($x39 (= (ite (or (and (not $x32) $x23) (and $x32 (not $x23))) (_ bv1 1) (_ bv0 1)) (_ bv0 1))))
 (let (($x40 (not $x39)))
 (let (($x41 (and $x40 $x40)))
 (let (($x42 (not $x41)))
 (let (($x52 (and $x42 $x42)))
 (let (($x53 (not $x52)))
 (let (($x54 (not $x53)))
 (let (($x48 (not (and (not (and (not $x42) $x42)) $x41))))
 (let (($x49 (and $x48 $x48)))
 (let (($x43 (not $x42)))
 (let (($x45 (and $x43 $x42)))
 (let (($x46 (not $x45)))
 (let (($x55 (and $x46 $x49)))
 (let (($x56 (and $x55 $x54)))
 (let (($x50 (and $x49 $x46)))
 (let (($x57 (and $x50 $x42)))
 (let (($x60 (not (not $x50))))
 (let (($x63 (not (not (and $x60 (and $x57 $x56))))))
 (and $x48 $x63))))))))))))))))))))))))
(check-sat-using dom-simplify)

commit: f810f25

[nunoplopes]

Reduced test case:

(assert
 (let (($x42 (not false)))
 (let (($x45 (and (not $x42) $x42)))
 (and (not $x45) $x42))))
(check-sat-using (then dom-simplify smt))
(check-sat)