Possible infinite loop with FP test
(set-logic FP)
(declare-const x (_ FloatingPoint 8 24))
(define-fun XIsNotNaN1 () Bool (not (fp.isNaN x)))
(define-fun XIsNotNaN2 () Bool (distinct x (_ NaN 8 24)))
(define-fun XIsNaN () Bool (fp.isNaN x))
(check-sat-assuming (XIsNotNaN1 XIsNaN))
(check-sat-assuming (XIsNotNaN2 XIsNaN))
Colibri2 seems to get stuck on the second check-sat-assuming
.