Soundness bug in QF_BVFP with dom-simplify tactic

[numairmansur]

HI @nunoplopes
On the following satisfiable file, I get unsat when using (check-sat-using dom-simplify)
110.zip

commit: c9be09b

[nunoplopes]

If you are doing automatic fuzzing, could you please reduce the files as well? It would help a lot the few Z3 folks. Thanks!

[numairmansur]

Let me try to reduce the file size

[numairmansur]

Reduced:

(set-option :print-success false)
(set-logic QF_BVFP)
(declare-fun symbolic_0_double_8874_ackermann!0 () (_ BitVec 64))
(assert
 (let (($x13 (and (fp.geq ((_ to_fp 11 53) symbolic_0_double_8874_ackermann!0) ((_ to_fp 11 53) (_ bv13831004815617530266 64))) (fp.leq ((_ to_fp 11 53) symbolic_0_double_8874_ackermann!0) ((_ to_fp 11 53) (_ bv4607632778762754458 64))))))
 (let (($x15 (not (not $x13))))
 (let (($x16 (not $x15)))
 (let (($x17 (not $x16)))
 (let (($x18 (and $x16 $x16)))
 (let (($x19 (and $x18 $x17)))
 (let (($x21 (not (and $x19 $x16))))
 (let (($x23 (not (and $x16 $x21))))
 (let (($x123 (not $x23)))
 (not $x123)))))))))))
(assert
 (let (($x13 (and (fp.geq ((_ to_fp 11 53) symbolic_0_double_8874_ackermann!0) ((_ to_fp 11 53) (_ bv13831004815617530266 64))) (fp.leq ((_ to_fp 11 53) symbolic_0_double_8874_ackermann!0) ((_ to_fp 11 53) (_ bv4607632778762754458 64))))))
 (let (($x15 (not (not $x13))))
 (let (($x16 (not $x15)))
 (not $x16)))))
(check-sat-using dom-simplify)

[nunoplopes]

Thanks.
Further reduced:

(assert
 (let (($x13 (and true true)))
 (let (($x15 (not (not $x13))))
 (let (($x16 (not $x15)))
 (let (($x17 (not $x16)))
 (not (and $x16 (not (and (and $x17))))))))))

(assert (not (not (and true true))))

(check-sat-using (then dom-simplify smt))
(check-sat)