$ cat a.smt2
(declare-fun ty_%a () (_ BitVec 2))
(declare-fun undef!1 () (_ FloatingPoint 8 24))
(assert (and (forall ((undef!0 (_ FloatingPoint 8 24)))
(let ((a!1 (fp.isNaN (fp.add roundNearestTiesToEven
((_ to_fp 8 24) (fp.to_ieee_bv undef!0))
(_ +zero 8 24))))
(a!2 (= (fp.add roundNearestTiesToEven
((_ to_fp 8 24) (fp.to_ieee_bv undef!0))
(_ +zero 8 24))
(fp.add roundNearestTiesToEven
((_ to_fp 8 24) (fp.to_ieee_bv undef!1))
(_ +zero 8 24)))))
(not (or a!1 a!2))))
(= ty_%a #b01)))
(check-sat)
$ z3 a.smt2 TRACE=true
ASSERTION VIOLATION
File: ../src/util/mpz.cpp
Line: 1791
numBits <= sizeof(unsigned)*8
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C
I see
ASSERTION VIOLATIONerror when running with TRACE=true.