Regression with floats

[nunoplopes]

Hi @wintersteiger!

The following test regressed with commit 9d57bdd
It gives sat now, and it used to be unsat (which I believe was correct).

(declare-fun undef!10 () (_ BitVec 32))
(declare-fun |#exists!21| () (_ BitVec 2))
(declare-fun |#exists!19| () Bool)
(declare-fun |#exists!18| () (_ BitVec 32))
(declare-fun |#exists!20| () Bool)

(assert (forall ((undef!0 (_ BitVec 32))
                    (undef!1 (_ BitVec 32))
                    (undef!2 (_ BitVec 32))
                    (undef!3 (_ BitVec 32))
                    (choice!8 (_ BitVec 2)))
             (! (let ((a!1 (ite (and |#exists!20|
                                     (= ((_ extract 30 0) |#exists!18|)
                                        #b0000000000000000000000000000000))
                                (concat (bvnot ((_ extract 31 31) |#exists!18|))
                                        ((_ extract 30 0) |#exists!18|))
                                |#exists!18|))
                      (a!2 (ite (= |#exists!21| #b10)
                                (fp.isNaN ((_ to_fp 8 24)
                                            (ite |#exists!19|
                                                 #x80000000
                                                 #x00000000)))
                                (= |#exists!21| #b11)))
                      (a!3 (ite (= ((_ extract 30 0) undef!1)
                                   #b0000000000000000000000000000000)
                                (concat (bvnot ((_ extract 31 31) undef!1))
                                        ((_ extract 30 0) undef!1))
                                undef!1))
                      (a!4 (or (= choice!8 #b01)
                               (and (not (= choice!8 #b10)) (= choice!8 #b11))))
                      (a!8 (ite (and (= ((_ extract 30 0) undef!10)
                                        #b0000000000000000000000000000000))
                                (concat (bvnot ((_ extract 31 31) undef!10))
                                        ((_ extract 30 0) undef!10))
                                undef!10))
                      (a!15 (fp.isNaN (fp.add roundNearestTiesToEven
                                              (_ -zero 8 24)
                                              (fp.neg ((_ to_fp 8 24) undef!1)))))
                      (a!18 (fp.isNaN (fp.add roundNearestTiesToEven
                                              (_ +zero 8 24)
                                              (fp.neg ((_ to_fp 8 24) undef!1))))))
                (let ((a!5 (not (ite (= choice!8 #b00)
                                     (fp.isNaN ((_ to_fp 8 24) a!3))
                                     a!4)))
                      (a!6 (fp.isNaN (fp.add roundNearestTiesToEven
                                             (_ -zero 8 24)
                                             (fp.neg ((_ to_fp 8 24) a!3)))))
                      (a!9 (not (fp.isNaN ((_ to_fp 8 24) a!8))))
                      (a!11 (fp.isNaN (fp.add roundNearestTiesToEven
                                              (_ +zero 8 24)
                                              (fp.neg ((_ to_fp 8 24) a!3)))))
                      (a!14 (not (ite (= choice!8 #b00)
                                      (fp.isNaN ((_ to_fp 8 24) undef!1))
                                      a!4)))
                      (a!16 (and (not (fp.isNaN ((_ to_fp 8 24) undef!1)))
                                 (not a!15)))
                      (a!19 (and (not (fp.isNaN ((_ to_fp 8 24) undef!1)))
                                 (not a!18))))
                (let ((a!7 (and (not (fp.isNaN ((_ to_fp 8 24) a!3)))
                                (not a!6)))
                      (a!12 (and (not (fp.isNaN ((_ to_fp 8 24) a!3)))
                                 (not a!11)))
                      (a!17 (or a!14 (not (or (not a!16) a!9))))
                      (a!20 (or a!14 (not (or (not a!19) a!9)))))
                (let ((a!10 (or a!5 (not (or (not a!7) a!9))))
                      (a!13 (or a!5 (not (or (not a!12) a!9)))))
                  (and (ite (= |#exists!21| #b00)
                            (fp.isNaN ((_ to_fp 8 24) a!1))
                            (or (= |#exists!21| #b01) a!2))
                       a!10
                       a!13
                       a!17
                       a!20))))))))
(check-sat)

[wintersteiger]

Yeah, looks like I was a bit too aggressive with the NaN encodings in the theory solver, sorry for the inconvenience!