(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun b () FPN)
(declare-fun c () FPN)
(declare-fun d () FPN)
(assert (= b (fp #b1 #b00001100001 #b0100111001011111011101101111000001100101111001101110)))
(assert (distinct c (fp #b1 #b01101101100 #b0111010000010010101100101111011100111100010001000110)))
(assert (= d (fp #b0 #b01101101100 #b0111010000010010101100101111011100111100010001000110)))
(assert (not (distinct (fp.sub roundNearestTiesToEven b c) d)))
(check-sat-using (then bit-blast ctx-solver-simplify))

ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 1865
!bits[!is_true][i]
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB