Assertion failure on FPA formula w/ NaNs

[nunoplopes]

$ z3 rewriter.hi_fp_unspecified=true nan.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 1803
val1 == val2

Call trace:

#1  smt::theory_bv::check_assignment(int) ()
#2  smt::theory_bv::final_check_eh() ()
#3  smt::context::final_check() ()
#4  smt::context::bounded_search() ()
#5  smt::context::search() ()
#6  smt::context::setup_and_check(bool) ()
#7  smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#8  and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()

nan.smt2.txt