Hi all,

In fp.neg the negation of NaN is ignored:

https://github.com/Z3Prover/z3/blob/master/src/ast/fpa/fpa2bv_converter.cpp#L700

I could not find any mention of this behavior in the SMT standard, only for fp.is_pos and fp.is_neg. I also tested it with MathSAT and SymFPU, and they seem to always flip the sign bit.

Is this the intended behavior?

Thanks.